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