Merge branch 'sail2' into rmem_interpreter

1 files changed, 3 insertions, 11 deletions

diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index 2dbd2bf4..f97c84a6 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -150,17 +150,9 @@ overload operator ^ = {xor_vec, int_power, concat_str}
 val mask : forall 'l 'm, 'l >= 0 & 'm >= 0. (implicit('l), bits('m)) -> bits('l)
 
 
-/* put this val spec into Sail lib for "%" */
-
-val mod = {
-  smt: "mod",
-  ocaml: "modulus",
-  lem: "integerMod",
-  c: "tmod_int",
-  coq: "Z.rem"
-} : forall 'M 'N. (int('M), int('N)) -> {'O, 0 <= 'O & 'O < N . int('O)}
-
-/* overload operator % = {mod_int} */
+overload operator % = {emod_int}
+overload operator / = {ediv_int}
+overload mod = {emod_int}
 
 val print = "print_endline" : string -> unit