Re: [isabelle] Rational numbers in Isabelle/ML

Thanks for sharing Manuel. I'm sure I can benefit from the pretty printing.
On Apr 2, 2016 08:44, "Manuel Eberl" <eberlm at> wrote:

> Hallo,
> I noticed that there is an ML implementation of rational numbers in the
> Isabelle distribution (~~/src/Tools/rat.ML).
> There are a few issues with this:
> â for some reason, it does not use operator overloading for
> addition/multiplication/equality/etc. on rational numbers, but introduces a
> "+/", "*/" etc. syntax for it.
> â pretty printing displays 1/3 and 1 as "Rat (1, 3)" and "Rat (1, 0)",
> respectively instead of "1 / 3" and "1". One could argue that "Rat (1, 3)"
> is the better choice since that means one can copy-paste output directly
> back as ML source again; however, it also makes output more difficult to
> read, in my opinion. At the very least, there should be a function that
> converts a rational number to such a string.
> â there is no functionality for parsing rational numbers at all (at least
> I couldn't find something like that)
> I have already implemented all of these things in my own little version of
> rational numbers (see attachment) and could merge any of them into the
> distribution if there is a consensus that that should be done.
> Any opinions?
> Cheers,
> Manuel

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