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

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

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)