source
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.

Instances For

source
@[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.

Instances For

source
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

Instances For