summaryrefslogtreecommitdiff
path: root/aarch64/prelude.sail
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/prelude.sail')
-rw-r--r--aarch64/prelude.sail7
1 files changed, 6 insertions, 1 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index ba5a3db7..55caddbb 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -105,7 +105,12 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys)
overload operator | = {or_bool, or_vec}
-val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+val UInt = {
+ ocaml: "uint",
+ lem: "uint",
+ interpreter: "uint",
+ c: "sail_uint"
+} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)