*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Rational numbers in Isabelle/ML*From*: Makarius <makarius at sketis.net>*Date*: Sun, 3 Apr 2016 14:01:23 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <57004746.6080409@in.tum.de>*References*: <56FEEB91.9060000@in.tum.de> <alpine.LNX.2.00.1604012351350.35180@lxbroy10.informatik.tu-muenchen.de> <56FFBBEF.1060602@in.tum.de> <alpine.LNX.2.00.1604022342050.55508@lxbroy10.informatik.tu-muenchen.de> <57004746.6080409@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sun, 3 Apr 2016, Manuel Eberl wrote:

* Rat.inv and MyRat.inv look odd to me, but for different reasons. Are these actually correct?There is a ~ missing in MyRat.inv. That code should definitely receive athorough review before it goes anywhere. Rat.inv looks fine to me.How about a formally specified and verified implementation? It should be mostly trivial with all the algebraic tools in Isabelle/HOL.

However, I would imagine that the exported could would be quite ugly.

Makarius

**Follow-Ups**:**Re: [isabelle] Rational numbers in Isabelle/ML***From:*Manuel Eberl

**References**:**[isabelle] Rational numbers in Isabelle/ML***From:*Manuel Eberl

**Re: [isabelle] Rational numbers in Isabelle/ML***From:*Makarius

**Re: [isabelle] Rational numbers in Isabelle/ML***From:*Manuel Eberl

**Re: [isabelle] Rational numbers in Isabelle/ML***From:*Makarius

**Re: [isabelle] Rational numbers in Isabelle/ML***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Rational numbers in Isabelle/ML
- Next by Date: Re: [isabelle] Rational numbers in Isabelle/ML
- Previous by Thread: Re: [isabelle] Rational numbers in Isabelle/ML
- Next by Thread: Re: [isabelle] Rational numbers in Isabelle/ML
- Cl-isabelle-users April 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list