diff options
Diffstat (limited to 'aarch64_small/prelude.sail')
| -rw-r--r-- | aarch64_small/prelude.sail | 14 |
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 |