[isabelle-dev] Multiset insert

[Tobias Nipkow]

On 28/07/2016 10:33, Peter Lammich wrote:
> On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote:
>> Tobias wrote:
>>
>>> How about
>>>
>>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
>>> "add# x M = {#x#} + M"
>
> This, however, may produce confusion with multiset union, which is an
> instance of the plus type classes, i.e., occupying the name
> plus_multiset.

I think that the type clarifies the difference. If this is a real concern, one 
could go for "add1" instead of "add". Since Jasmin and Mathias have been working 
with and on multisets a lot, they are in a good position to judge which 
alternative works better.

Tobias

> --
>   Peter
>
>
>>
>> Lovely!
>>
>> Jasmin
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
> _______________________________________________
> 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/a36d118e/attachment.bin>