[isabelle-dev] Multiset insert

Jasmin Blanchette jasmin.blanchette at inria.fr
Wed Jul 27 11:39:28 CEST 2016

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

i.e. with #∪ instead of +. How about "add"?

    add x M = {#x#} + M

Or "add1"? Or "add_mset" etc.?


More information about the isabelle-dev mailing list