Zulip Chat Archive

Stream: general

Topic: Multiset Coe


view this post on Zulip 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)⟩

view this post on Zulip Eric Wieser (Mar 18 2021 at 23:20):

Are you looking for docs#multiset.sort?

view this post on Zulip Eric Wieser (Mar 18 2021 at 23:21):

to_list is noncomputable because it doesn't specify an order

view this post on Zulip 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