> but this leads to the rather lengthy "insert_mset x M" as opposed to the
> current "{#x#} + M". This would come up in all inductive proofs. If we want
> to mimic sets, it actually seems unavoidable...
With completion, it might actually be easier to type "insert_mset x M" than
"{#x#} + M".
Although I suggested we do this, and still think logically it is the right thing
to do, I see one issue, the naming of insert#. The canonical name is
insert_mset, but this leads to the rather lengthy "insert_mset x M" as opposed
to the current "{#x#} + M". This would come up in all inductive
Hi all,
in recent private discussion the question was raised whether the
explicit representation of multisets should follow that of sets.
For sets, we have:
{a, b, c} = insert a (insert b (insert c empty))
For multisets, we currently have:
{#a, b, c#} = single a + single b +
