[isabelle-dev] NEWS: Lexically unsigned numerals for HOL
makarius at sketis.net
Mon Sep 22 20:50:57 CEST 2014
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
I have presently something that might soon become a changeset to remove
the xnum token syntax from Pure.
More information about the isabelle-dev