[isabelle-dev] NEWS: Lexically unsigned numerals for HOL

Florian Haftmann 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,


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140921/03894060/attachment.asc>

More information about the isabelle-dev mailing list