Very good! This is very convenient.
On 01/06/16 21:42, Makarius wrote:
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing.
On 01/06/16 21:47, Lawrence Paulson wrote:
> Doesn’t Poly/ML include an option to support GCDs (if not rationals)
> efficiently?
Do you mean PolyML.IntInf.gcd and PolyML.IntInf.lcm? That is already
used (da38571dd5bd).
These operations normally use GNU MP, but on Mac OS X only the old
builtin
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
> * Structure Rat for rational numbers is now an integral part of
> Isabelle/ML, with special notation @int/nat or @int for numerals (an
> abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
> printing. Standard operations on type Rat.rat are provided via ad-hoc
> overloading of + -
