HepLean Documentation

Init.Data.Array.QSort

def Array.qpartition {α : Type u_1} (as : Array α) (lt : ααBool) (lo hi : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[irreducible]
    def Array.qpartition.loop {α : Type u_1} (lt : ααBool) (hi : Nat) (this : Inhabited α) (pivot : α) (as : Array α) (i j : Nat) :
    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) (low : Nat := 0) (high : Nat := as.size - 1) :
      Equations
      Instances For
        @[specialize #[]]
        partial def Array.qsort.sort {α : Type u_1} (lt : ααBool) (as : Array α) (low high : Nat) :
        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