[isabelle-dev] proposal for new numeral representation

[Florian Haftmann]

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

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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