Re: [isabelle] Target language bindings for rat



There is an implementation used in HOL4 at

https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/portableML/Arbrat.{sig,sml}



Michael

> On 17 Dec 2015, at 03:58, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> 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
>

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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