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: May 16 2021 at 05:21 UTC