Re: [isabelle] Rational numbers in Isabelle/ML

I don't think this is relevant to isabelle-users. Rat is just one of many auxiliary modules in the implementation.
I have one entry in the AFP already that uses rational numbers in ML, and another AFP submission is in preparation. I think this is definitely relevant to some Isabelle users (e.g. for automatically providing witnesses for certain things; in my case, solutions to linear programs and adequate interval splittings for Sturm's method).

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.

* is the only canonical operation from that structure, everything else should be ignored.
All right, then what is the canonical way to do things like that? Nested case statements? Those can get very ugly and unreadable very fast.



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