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

  * 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:


    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.


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