mathlib3 documentation

core / init.data.list.qsort

def list.qsort.F {α : Type u_1} (lt : α α bool) (x : list α) :
(Π (y : list α), y.length < x.length list α) list α
Equations
def list.qsort {α : Type u_1} (lt : α α bool) :
list α list α

This is based on the minimalist Haskell "quicksort".

Remark: this is not really quicksort since it doesn't partition the elements in-place

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 = bool.tt) t)