Commit c3f99bd1 authored by MARCHE Claude's avatar MARCHE Claude

fixed syntax errors in polypaver examples

parent d7f08f7b
......@@ -3,6 +3,7 @@ module TestFloat
use import floating_point.Double
(*
function Sqrt (X : in Float) return Float
pre 1.0 <= X and X <= 2.0;
......@@ -21,3 +22,7 @@ pre 1.0 <= X and X <= 2.0;
end loop;
return R;
end Sqrt;
*)
end
\ No newline at end of file
......@@ -17,7 +17,7 @@ theory TestReal
use import real.ExpLog
goal exp_hyp:
forall x:real. 0.01 < X < 5.1785 ->
forall x:real. 0.01 < x < 5.1785 ->
(3.0 + sqr x / 11.0) * ((exp x - exp (-x))/2.0) <
x * (2.0 + (exp x + exp (-x))/2.0 + sqr x / 11.0)
......
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