Commit 693cf003 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make sure that RealInfix.(-.) unfolds to Real.(-).

parent 68d34132
......@@ -15,10 +15,3 @@ Require Import BuiltIn.
Require BuiltIn.
Require real.Real.
(* Why3 goal *)
Lemma infix_mndt_def : forall (x:R) (y:R), ((x - y)%R = (x + (-y)%R)%R).
Proof.
intros x y.
reflexivity.
Qed.
......@@ -7,7 +7,7 @@ f93d912698cd9b10846cd861492655f1c6cf9ab0 int/MinMax.xml
9e550b757adffdb78db010e8aa14b85a065b3c60 int/Power.xml
79ca42a9fba90deb0e8eb7fb5396de8a756ac969 bool/Bool.xml
6bb79ae3bc3abb9b0710a2dfd58c0bd2c41b8f13 real/Real.xml
657f5992027dc0d739351289093cac512a534fcb real/RealInfix.xml
f80da4609433de4d5ccb6ebbbe0fa954c5ed5187 real/RealInfix.xml
c2410d334c7e0852086bb13cae1189f601f3b1c6 real/Abs.xml
da70a842eac8ff6687f1d119c309be4c227976ff real/MinMax.xml
3cc6bd97503e596fae70c51ef1d5401a62114b94 real/FromInt.xml
......
......@@ -20,7 +20,6 @@ module Real
val function (*) real real : real
val predicate (<) real real : bool
let (-) (x y : real) = x + -y
let predicate (>) (x y : real) = y < x
let predicate (<=) (x y : real) = x < y || x = y
let predicate (>=) (x y : real) = y <= x
......@@ -30,6 +29,10 @@ module Real
function (-_) = (-_), function (+) = (+),
function (*) = (*), predicate (<=) = (<=)
let (-) (x y : real)
ensures { result = x - y }
= x + -y
val (/) (x y:real) : real
requires { y <> 0.0 }
ensures { result = x / y }
......
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