[isabelle-dev] NEWS: Lexically unsigned numerals for HOL
florian.haftmann at informatik.tu-muenchen.de
Sun Sep 21 17:04:08 CEST 2014
After realising that HOL and ZF numerals are already separate lexical
categories (though the history of this being so ist not clear to me at
the moment), I finally took the adventure of turning HOL numerals into
unsigned numerals also lexically (logically, this has already been the
case for a long time). See now 6d46ad54a2ab.
Two issues remain left to settle on.
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.
Awaiting your suggestions and advice,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev