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).
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.
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. [â]
* Option.map 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