>> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
