@[inline]

def Array.qpartition {α : Type u_1} {n : Nat} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega) (hlo : lo < n := by omega) (hhi : hi < n := by omega) : { m : Nat // lo ≤ m ∧ m ≤ hi } × Vector α n

Internal implementation of Array.qsort.

qpartition as lt lo hi hlo hhi returns a pair (⟨m, h₁, h₂⟩, as') where as' is a permutation of as and m is a number such that:

• lo ≤ m
• m < n
• ∀ i, lo ≤ i → i < m → lt as[i] as[m]
• ∀ j, m < j → j < hi → !lt as[j] as[m]

It does so by first swapping the elements at indices lo, mid := (lo + hi) / 2, and hi if necessary so that the middle (pivot) element is at index hi. We then iterate from k = lo to k = hi, with a pointer i starting at lo, and swapping each element which is less than the pivot to position i, and then incrementing i.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Array.qsort {α : Type u_1} (as : Array α) (lt : α → α → Bool := by exact (· < ·)) (lo : Nat := 0) (hi : Nat := as.size - 1) : Array α

In-place quicksort.

qsort as lt lo hi sorts the subarray as[lo...=hi] in-place using lt to compare elements.

Equations

• One or more equations did not get rendered due to their size.

def Array.qsortOrd {α : Type u_1} [ord : Ord α] (xs : Array α) : Array α

Sort an array using compare to compare elements.

Equations

• xs.qsortOrd = xs.qsort fun (x y : α) => (compare x y).isLT