Construct a sorted list from a multiset. #

def Multiset.sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
List α

sort s constructs a sorted list from the multiset s. (Uses merge sort algorithm.)

Equations
Instances For
@[simp]
theorem Multiset.coe_sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (l : List α) :
=
@[simp]
theorem Multiset.sort_sorted {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
@[simp]
theorem Multiset.sort_eq {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
() = s
@[simp]
theorem Multiset.mem_sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] {s : } {a : α} :
a a s
@[simp]
theorem Multiset.length_sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] {s : } :
().length = Multiset.card s
@[simp]
theorem Multiset.sort_zero {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] :
= []
@[simp]
theorem Multiset.sort_singleton {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (a : α) :
Multiset.sort r {a} = [a]
unsafe instance Multiset.instRepr {α : Type u_1} [Repr α] :
Repr ()
Equations
• One or more equations did not get rendered due to their size.