diff options
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Makefile | 2 | ||||
| -rw-r--r-- | lib/coq/Sail2_real.v | 18 |
2 files changed, 19 insertions, 1 deletions
diff --git a/lib/coq/Makefile b/lib/coq/Makefile index 99321aae..a5f2874b 100644 --- a/lib/coq/Makefile +++ b/lib/coq/Makefile @@ -1,6 +1,6 @@ BBV_DIR=../../../bbv/theories -SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_string.v +SRC=Sail2_prompt_monad.v Sail2_prompt.v Sail2_impl_base.v Sail2_instr_kinds.v Sail2_operators_bitlists.v Sail2_operators_mwords.v Sail2_operators.v Sail2_values.v Sail2_state_monad.v Sail2_state.v Sail2_string.v Sail2_real.v COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v new file mode 100644 index 00000000..49023d4c --- /dev/null +++ b/lib/coq/Sail2_real.v @@ -0,0 +1,18 @@ +Require Export Rbase. +Require Import Reals. +Require Export ROrderedType. + +Definition realFromFrac (num denom : Z) : R := Rdiv (IZR num) (IZR denom). + +Definition gteq_real (x y : R) : bool := if Rge_dec x y then true else false. +Definition lteq_real (x y : R) : bool := if Rle_dec x y then true else false. +Definition gt_real (x y : R) : bool := if Rgt_dec x y then true else false. +Definition lt_real (x y : R) : bool := if Rlt_dec x y then true else false. + +(* Export select definitions from outside of Rbase *) +Definition powerRZ := powerRZ. +Definition Rabs := Rabs. + +(* Use flocq definitions, but without making the whole library a dependency. *) +Definition Zfloor (x : R) := (up x - 1)%Z. +Definition Zceil (x : R) := (- Zfloor (- x))%Z. |