Merge branch 'minimum-excludant-other-versions' into 'master'
[why3.git] / examples / logic / real.why
blobe61ae95042974487fee0afcbfd4f3e8725af4208
1 theory CosineSingle
3 use real.Real
4 use real.Abs
5 use real.Trigonometry
7 (* approximation of cosine function by 1 - x^2 / 2 on interval [-1/32; 1/32] *)
11 lemma MethodError: forall x:real. abs x <= 0x1p-5 ->
12   abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24
13 (* this one is proved in Coq + interval tactics *)
16 end