On 01/06/16 21:58, Florian Haftmann wrote: > > One could regard the dedicated literal syntax for rationals a little bit > oversophisticated; maybe an infix // for Rat.make would serve better. > Or we could A matter of personal taste, though.
There is a delicate point here: our antiquotation infrastructure
distinguishes inlined text from compile-time values. @a/b is the latter,
so it is always guaranteed to be pre-evaluated, independently of other
code inline options of Poly/ML.
This is also the reason why I have removed Rat.zero, Rat.one, Rat.two
and used @0, @1, @2 everywhere.
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
