diff options
Diffstat (limited to 'lib/arith.sail')
| -rw-r--r-- | lib/arith.sail | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index a3a80fc5..8825ac2f 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -70,7 +70,11 @@ val _shl_int = "shl_int" : (int, int) -> int overload shl_int = {_shl8, _shl32, _shl_int} -val shr_int = "shr_int" : (int, int) -> int +val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)} + +val _shr_int = "shr_int" : (int, int) -> int + +overload shr_int = {_shr32, _shr_int} // ***** div and mod ***** @@ -98,6 +102,7 @@ val abs_int = { smt : "abs", ocaml: "abs_int", lem: "abs_int", + c: "abs_int", coq: "Z.abs" } : (int, int) -> int |