Re: [isabelle] Target language bindings for rat
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,
On 2015-12-16 16:48, Andreas Lochbihler wrote:
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 (https://github.com/non/spire), but I have not found anything
for SML. Does anyone know of such a library for SML?
University of Cambridge
This archive was generated by a fusion of
Pipermail (Mailman edition) and