diff options
Diffstat (limited to 'theories/Floats/FloatAxioms.v')
| -rw-r--r-- | theories/Floats/FloatAxioms.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v index d057d641da..d835e87ee0 100644 --- a/theories/Floats/FloatAxioms.v +++ b/theories/Floats/FloatAxioms.v @@ -22,7 +22,16 @@ Qed. Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x). Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x). -Axiom compare_spec : forall x y, (x ?= y)%float = SFcompare (Prim2SF x) (Prim2SF y). + +Definition flatten_cmp_opt c := + match c with + | None => FNotComparable + | Some Eq => FEq + | Some Lt => FLt + | Some Gt => FGt + end. +Axiom compare_spec : forall x y, (x ?= y)%float = flatten_cmp_opt (SFcompare (Prim2SF x) (Prim2SF y)). + Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). Axiom add_spec : forall x y, Prim2SF (x + y)%float = SF64add (Prim2SF x) (Prim2SF y). Axiom sub_spec : forall x y, Prim2SF (x - y)%float = SF64sub (Prim2SF x) (Prim2SF y). |