> 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.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
