## Stream: general

### Topic: Multiset Coe

#### Scott Viteri (Mar 18 2021 at 22:58):

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 (Mar 18 2021 at 23:20):

Are you looking for docs#multiset.sort?

#### Eric Wieser (Mar 18 2021 at 23:21):

to_list is noncomputable because it doesn't specify an order

#### Scott Viteri (Mar 18 2021 at 23:26):

Yes this is what I was looking for, thanks!

Last updated: May 16 2021 at 05:21 UTC