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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev