diff options
| author | Alasdair Armstrong | 2018-01-30 15:06:20 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-30 15:11:14 +0000 |
| commit | 368e8b200d53611ca145c63a876a6d37fcf5acaf (patch) | |
| tree | 561d0ef1bbcf8d0c650e846f10a9b00f303c532c /riscv | |
| parent | 2a14c291caa7b07ac1e3ed6904765ea8702a4818 (diff) | |
Fix failing Lem tests
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 19b8abd8..370f9370 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -2,7 +2,6 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None, Some : 'a} -infix 4 == val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -251,14 +250,10 @@ val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> r val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int -infixl 7 / - overload operator / = {quotient_nat, quotient, quotient_real} val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int -infixl 7 % - overload operator % = {modulus} val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real |