def
Array.qpartition
{α : Type u_1}
{n : Nat}
(as : Vector α n)
(lt : α → α → Bool)
(lo hi : Nat)
(hlo : lo < n := by omega)
(hhi : hi < n := by omega)
:
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 ≤ mm < 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 j = lo to j = 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
@[irreducible]
def
Array.qpartition.loop
{α : Type u_1}
{n : Nat}
(lt : α → α → Bool)
(lo hi : Nat)
(hhi : hi < n := by omega)
(pivot : α)
(as : Vector α n)
(i j : Nat)
(ilo : lo ≤ i := by omega)
(jh : j < n := by omega)
(w : i ≤ j := by omega)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
def
Array.qsort
{α : Type u_1}
(as : Array α)
(lt : α → α → Bool := by exact (· < ·))
(low : Nat := 0)
(high : Nat := as.size - 1)
:
Array α
In-place quicksort.
qsort as lt low high sorts the subarray as[low:high+1] in-place using lt to compare elements.
Equations
- One or more equations did not get rendered due to their size.