summaryrefslogtreecommitdiff
path: root/lib/arith.sail
diff options
context:
space:
mode:
Diffstat (limited to 'lib/arith.sail')
-rw-r--r--lib/arith.sail4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
index 6ddc58aa..af814c81 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -57,13 +57,13 @@ let elsize = shl_int(8, UInt(size))
```
THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
*/
-val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
+val _shl8 = {c: "shl_mach_int", coq: "shl_int_8", _: "shl_int"} :
forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)}
/*!
Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
*/
-val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
+val _shl32 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} :
forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)}
val _shl_int = "shl_int" : (int, int) -> int