[isabelle-dev] NEWS: Rat in Isabelle/ML
makarius at sketis.net
Wed Jun 1 22:01:08 CEST 2016
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev