Zulip Chat Archive

Stream: general

Topic: Multiset Coe

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

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: Aug 03 2023 at 10:10 UTC