[isabelle-dev] Explicit representation of multisets

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Mar 10 10:53:41 CET 2016

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 + single c

But the following would also be possible:
	{#a, b, c#} = insert# a (insert# b (insert# c empty#))

Is there any evidence that we should not attempt this?



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160310/97a5d9fe/attachment.asc>

More information about the isabelle-dev mailing list