[isabelle-dev] NEWS: Lexically unsigned numerals for HOL
nipkow at in.tum.de
Sun Sep 21 17:24:50 CEST 2014
On 21/09/2014 17:04, Florian Haftmann wrote:
> 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.
At last I can write "n-1" without getting a complaint that n cannot be applied
to -1. Hurray, and thanks a lot for that!
> 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, Florian
> _______________________________________________ isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev