[isabelle-dev] NEWS: Lexically unsigned numerals for HOL
lp15 at cam.ac.uk
Mon Sep 22 15:25:48 CEST 2014
The situation involving ZF can go either way, as there are hardly any users.
How are negative integers written in ZF now? Can one still write #-3 or is it $- #3?
On 21 Sep 2014, at 16:04, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> 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.
> 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:
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev