diff options
| author | Brian Campbell | 2018-07-02 17:56:23 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-02 18:49:29 +0100 |
| commit | fe5e67979d26bfa3c8c51863b24d97ab5553d56b (patch) | |
| tree | 86593f222029a07ad70dd5ed752345f984abc3fd /mips/prelude.sail | |
| parent | e6b40776a3c963ad3d16b644ba283d2d955cf0b5 (diff) | |
Coq modulus operation that fits the type
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index c411ad83..b3349799 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -104,7 +104,7 @@ overload operator / = {quotient_nat, quotient} val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", coq: "Z.quot", _ : "tdiv_int"} : (int, int) -> int val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", coq: "Z.rem", _ : "tmod_int"} : (int, int) -> int -val modulus = {ocaml: "modulus", lem: "hardware_mod", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) +val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) overload operator % = {modulus} |