Documentation

Init.Data.Array.QSort

@[inline]
def Array.qsort {α : Type u_1} (as : Array α) (lt : ααBool := by exact (· < ·)) (low : Nat := 0) (high : Nat := as.size - 1) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[irreducible, specialize #[]]
    def Array.qsort.sort {α : Type u_1} (lt : ααBool := by exact (· < ·)) {n : Nat} (as : Vector α n) (lo hi : Nat) (hlo : lo < n := by omega) (hhi : hi < n := by omega) :
    Vector α n
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Array.qsortOrd {α : Type u_1} [ord : Ord α] (xs : Array α) :

      Sort an array using compare to compare elements.

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