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

[Tobias Nipkow]

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!

Tobias

> 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 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>