Initial commit for proving arith. emulation of succ & pred

Co-authored-by: Benjamin Peyrille <[email protected]> Co-authored-by: Pierre Roux <[email protected]> Co-authored-by: Erik Martin-Dorel <[email protected]>
validsdp · Dec 18, 2020 · 2a937c0 · 2a937c0
1 parent 7025a93
commit 2a937c0
Show file tree

Hide file tree

Showing 2 changed files with 1,779 additions and 0 deletions.
diff --git a/Remakefile.in b/Remakefile.in
@@ -26,6 +26,7 @@ FILES = \
 	Prop/Sterbenz.v \
 	Prop/Round_odd.v \
 	Prop/Double_rounding.v \
+	Prop/Emulated_succ_pred.v \
 	@PRIM_FLOAT@ \
 	IEEE754/SpecFloatCompat.v \
 	IEEE754/BinarySingleNaN.v \