Zulip Chat Archive

Stream: general

Topic: multiset.erased_dup


matt rice (Jan 03 2021 at 23:21):

Is it weird that multiset.erase_dup https://github.com/leanprover-community/mathlib/blob/master/src/data/multiset/erase_dup.lean#L19-L20 docs says "yielding a nodup multiset." but the return value is plain multiset, e.g. doesn't seem to have any multiset.nodup, if so would that be a doc issue, definition issue, or me missing something perhaps?

Floris van Doorn (Jan 03 2021 at 23:23):

docs#multiset.nodup_erase_dup?

matt rice (Jan 03 2021 at 23:33):

aha :dizzy:, thanks.


Last updated: Dec 20 2023 at 11:08 UTC