Re: [isabelle] Rational numbers in Isabelle/ML



On Sat, 2 Apr 2016, Manuel Eberl wrote:

 This follows Standard ML. Adhoc overloading is not defined by the language
 and works differently in each implementation. [â] we can in principle
 become more specific to a particular Poly/ML version. [â]

I don't really have any opinion on this. Uniform notation for addition etc. is nice to have, but I cannot say whether it is worth it. This is one of the reasons why I wrote that email, to collect some more opinions on the issue.

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

Looking at the Poly/ML sources, its internal addOverload operation has a comment as follows:

  (* This goes in RunCall since it's only for the basis library. *)

In Isabelle/bb29cc00c31f I have already removed that critical bootstrap structure from the ML environment: it contains other things that may disrupt the ML system in a bad way (similar to Obj.magic in OCaml).


So if the overloaded syntax should be used, it needs to be part of the Isabelle/Pure bootstrap environment. In that case one could also invent separate notation for rat literals and make that an integral part of Isabelle/ML.

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.


	Makarius


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