Re: [isabelle] Target language bindings for rat

Hi Andreas,

As far as I know, src/Tools/rat.ML is an implementation of rational number in Isabelle/ML and MetiTarski ( uses another implementation that is inherited from John Harrison somehow.

I have considered this question before, but considering there is no standard implementation of rational number in the standard PolyML library, I thought it is risky to do such binding...

Hope this helps,

On 2015-12-16 16:48, Andreas Lochbihler wrote:
Dear all,

I am looking for bindings of rational numbers to the target languages
of the code generator. Has anyone done something in this direction?
E.g., something analogous to Code_Numeral.integer and

Haskell and OCaml support arbitrary-precision rational numbers in
their libraries (Rational and Num.num) and there is a library for
Scala (, but I have not found anything
for SML. Does anyone know of such a library for SML?


Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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