core / init.data.list.qsort

def list.qsort.F {α : Type u_1} (lt : α → α → bool) (x : list α) :

Equations

list.qsort.F lt (h :: t) IH = (λ (_x : list α × list α) (e : list.partition (λ (x : α), lt h x = bool.tt) t = _x), prod.rec (λ (large small : list α) (e : list.partition (λ (x : α), lt h x = bool.tt) t = (large, small)), IH small _ ++ h :: IH large _) _x e) (list.partition (λ (x : α), lt h x = bool.tt) t) _
list.qsort.F lt list.nil IH = list.nil

def list.qsort {α : Type u_1} (lt : α → α → bool) :

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)