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:
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
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
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
