> 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?
The first one. Numerals in ZF are left as they are, *signed*.
Florian
--
PGP available:
http://home.informatik.tu
On Mon, 22 Sep 2014, Makarius wrote:
Looking once again at ZF xnum syntax, I think it can be expressed
without the xnum token, and without any syntax change for now -- that
may be reconsidered independently.
See now:
changeset: 58420:37cbbd8eb460
user:wenzelm
date:Mon Sep 2
On Sun, 21 Sep 2014, Florian Haftmann wrote:
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 sourc
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?
Larry
On 21 Sep 2014, at 16:04, Florian Haftmann
wrote:
> After realising that HOL and ZF numerals are already separate lexical
>
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
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
