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
-- PeterLovely! Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ 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
