diff options
| author | Jon French | 2019-02-03 17:50:01 +0000 |
|---|---|---|
| committer | Jon French | 2019-02-03 17:50:01 +0000 |
| commit | ab3f3671d4dd682b2aee922d5a05e9455afd5849 (patch) | |
| tree | d951e1beac8fa0af18c71e6c33879925b2707049 /lib/coq/Sail2_values.v | |
| parent | bce4ee6000254c368fc83cdf62bdcdb9374b9691 (diff) | |
| parent | 4f45f462333c5494a84886677bc78a49c84da081 (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'lib/coq/Sail2_values.v')
| -rw-r--r-- | lib/coq/Sail2_values.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index e3e039c2..219a6f84 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -9,6 +9,7 @@ Require Export List. Require Export Sumbool. Require Export DecidableClass. Require Import Eqdep_dec. +Require Export Zeuclid. Import ListNotations. Open Scope Z. @@ -1654,8 +1655,8 @@ end (* Arithmetic functions which return proofs that match the expected Sail types in smt.sail. *) -Definition div_with_eq n m : {o : Z & ArithFact (o = Z.quot n m)} := build_ex (Z.quot n m). -Definition mod_with_eq n m : {o : Z & ArithFact (o = Z.rem n m)} := build_ex (Z.rem n m). +Definition ediv_with_eq n m : {o : Z & ArithFact (o = ZEuclid.div n m)} := build_ex (ZEuclid.div n m). +Definition emod_with_eq n m : {o : Z & ArithFact (o = ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m). Definition abs_with_eq n : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n). (* Similarly, for ranges (currently in MIPS) *) |