[isabelle-dev] Infix syntax for division?
florian.haftmann at informatik.tu-muenchen.de
Tue Jun 2 21:18:27 CEST 2015
> I believe Maude (another system named after a French female, presumably) even had a different minus operator on “nat” as opposed to the other types. In a formal context, such precision is surely helpful. Indeed, minus is a nasty case for Dmitriy’s coercions.
If there an established infix notation more confined minus, we could use
this likewise using abbreviations (hence avoiding duplication on the
logical level). But that is another story.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev