# Re: [isabelle] Rational numbers in Isabelle/ML

On Sat, 2 Apr 2016, Makarius wrote:

It would be certainly nice to have +, -, *, / on type rat.

`Isabelle/ML is an "embrace and extend" version of Standard ML -- what SML
``could have been if it had not been hindered by SML/NJ. Nonetheless, adding
``new things to Isabelle/ML requires some care.
`

There are two syntax questions here:
* Overloaded +, -, *, / etc. as for the other SML Basis number
implementations. Poly/ML provides an internal operation for that,
which happens to be publicly available, at least during Isabelle/Pure
bootstrap.
* Notation for literals. We have already antiquotations in Isabelle/ML,
even short forms with control symbols and cartouches. This could be
probably stretched one step further to introduce the following syntax:
#DIGITS/DIGITS or #~DIGITS/DIGITS
As abbreviation for @{rational ...} with the usual meaning of
antiquotations. In particular, a "value" antiquotation produces
results as static values only once at compile-time.

`Such advanced ML surface syntax requires a truely advanced implementation
``behind it, beyond any doubts about correctness and performance.
`
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*