Multiset Coe

Stream: general

[Scott Viteri]

Hello,
I am looking for a function from multisets to lists that repeats each element x as needed.
I see to_list, but this is noncomputable definition using choice.
Alternately, if I can get a list of unique elements of the multiset, I can do something like

instance lift_multiset : has_lift (multiset ℕ) (list ℕ) :=
 ⟨λ m, join $ map (λ n, list.repeat n (count n m)) (uniq_elems m)⟩

[Eric Wieser]

Are you looking for docs#multiset.sort?

[Eric Wieser]

to_list is noncomputable because it doesn't specify an order

[Scott Viteri]

Yes this is what I was looking for, thanks!