Re: [isabelle] Rational numbers in Isabelle/ML
That should be quite possible, and I expect the proofs to be very easy,
if not completely automatic.
On 03/04/16 14:01, Makarius wrote:
On Sun, 3 Apr 2016, Manuel Eberl wrote:
* Rat.inv and MyRat.inv look odd to me, but for different
There is a ~ missing in MyRat.inv. That code should definitely
receive a thorough review before it goes anywhere. Rat.inv looks fine
these actually correct?
How about a formally specified and verified implementation? It
mostly trivial with all the algebraic tools in Isabelle/HOL.
However, I would imagine that the exported could would be quite ugly.
I did not mean to use exported code, but just to make a demo theory
with all the definitions and maybe some simple proofs (e.g. in
HOL/ex). The idea is just to make certain intentions and invariants
explicit, notably the sign of certain parts.
A related question is about sign in lcm/gcd: in structure Integer,
PolyML.IntInf, and the HOL definitions. There is also a connection of
PolyML.IntInf operations with the code generator in AFP Gauss_Jordan
This archive was generated by a fusion of
Pipermail (Mailman edition) and