mathlib documentation

core / init.data.list.qsort

def list.qsort.F {α : Type u_1} (lt : α → α → bool) (x : list α) :
(Π (y : list α), y.length < x.lengthlist α)list α
Equations
def list.qsort {α : Type u_1} (lt : α → α → bool) :
list αlist α
Equations
@[simp]
theorem list.qsort_nil {α : Type u_1} (lt : α → α → bool) :
@[simp]
theorem list.qsort_cons {α : Type u_1} (lt : α → α → bool) (h : α) (t : list α) :
list.qsort lt (h :: t) = (λ (_a : list α × list α), _a.cases_on (λ (fst snd : list α), id_rhs (list α) (list.qsort lt snd ++ h :: list.qsort lt fst))) (list.partition (λ (x : α), lt h x = tt) t)