[isabelle-dev] proposal for new numeral representation
florian.haftmann at informatik.tu-muenchen.de
Fri Nov 25 20:42:26 CET 2011
>> class neg_numeral = group_add + one
>> definition (in neg_numeral) neg_numeral :: "bin => 'a" where
>> "neg_numeral k = - numeral k"
> Is there a conceptual point for neg_numeral, beyond concrete syntax issues?
> One could just use regular uminus, but then there will be an accidental
> change in concrete syntax: -42 and - 42 would be the same, both with the
> weaker priority of unary minus.
This can be done at a later stage. The first step is to pull the sign
out of the representation to topmost position, which makes life already
a lot easier.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev