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
Equations
- list.qsort lt = list.qsort._proof_1.fix (list.qsort.F lt)
@[simp]
@[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)