On Sun, 21 Sep 2014, Florian Haftmann wrote:
a) Currently, the prefix for (signed!) ZF numerals is »#«. Since
operations for integers in ZF are mainly associated with »$« (e.g., »_
$+ _«, »_ $* _«), maybe it would be more consistent to prefer »$« also
here. As far as I understand from the sources, ZF numerals are not
polymorphic but restricted to set int in ZF.
b) The lexical category for signed numerals is named »xnum«. Maybe
»signed_num« would be more explicit.
The "x" in "xnum" can be explained historically as a special marker for
something that is a numeral with some extra decoration. The signed vs.
unsigned aspect came much later, and was not there in distant past.
Looking once again at ZF xnum syntax, I think it can be expressed without
the xnum token, and without any syntax change for now -- that may be
reconsidered independently.
I have presently something that might soon become a changeset to remove
the xnum token syntax from Pure.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
