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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and