Commit 13235416 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some obsolete conversions between machine integers and unbounded integers.

parent 7345cf60
......@@ -101,10 +101,10 @@ module EuclideanAlgorithm31
let rec euclid (u v: int31) : int31
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
=
if Int31.eq v (of_int 0) then
if v = 0 then
u
else
euclid v (u % v)
......@@ -119,10 +119,10 @@ module EuclideanAlgorithm63
let rec euclid (u v: int63) : int63
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
= "vc:sp"
if v = of_int 0 then
if v = 0 then
u
else
euclid v (u % v)
......
......@@ -125,7 +125,7 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm63" proved="true" sum="b8b13e83f3d237bbc360c6f9f88ef153">
<theory name="EuclideanAlgorithm63" proved="true" sum="2957f2c27fa5f1ab089e561053c1d9ac">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment