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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
