[isabelle-dev] Multiset insert

[Tobias Nipkow]

On 27/07/2016 11:39, Jasmin Blanchette wrote:
> Tobias wrote:
>
>> Did we ever discuss the naming issue? "insert_mset" would be the canonical name, but it would make larger expressions hard to read.
>
> I'm not so sure "insert_mset" would be the right name. Its set-based terminology might suggest a definition like
>
>     insert_mset x M = {#x#} #∪ M

You have a point. I didn't even realize that we have #∪.

> i.e. with #∪ instead of +. How about "add"?
>
>     add x M = {#x#} + M
>
> Or "add1"? Or "add_mset" etc.?

I am all in favour of a variation of "add" - it corresponds nicely to "+". Of 
course not "add" by itself, that is too generic. How about

definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
"add# x M = {#x#} + M"

Tobias

> Jasmin
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160728/a904079c/attachment.bin>