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 (https://bitbucket.org/lcpaulson/metitarski/src) 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,
Wenda

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
Code_Target_Int.thy?

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

Best,
Andreas

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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