[isabelle-dev] proposal for new numeral representation

Florian Haftmann 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.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111125/789a37b2/attachment.sig>

More information about the isabelle-dev mailing list