> On 28.07.2016, at 10:33, Peter Lammich <lamm...@in.tum.de> 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's fair enough, because we operate in a simply typed setting.
Logicians and computer scientists frequently use the same symbol for both
operations, namely comma, when writing contexts in logical or typing judgments.
E.g.
\Gamma, t : \tau
\Gamma, \Delta
t : \tau, \Gamma
Without going quite that far here (nor can we due to the type of +), this shows
that two think of "add_mset" and + as "essentially the same thing" is not too
far off the mark.
"add1_mset" resp. "add1#" would make things more explicit, but since there's
hardly any confusion possible there's also hardly any need to make things
explicit.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
