summaryrefslogtreecommitdiff
path: root/aarch64/prelude.sail
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/prelude.sail')
-rwxr-xr-xaarch64/prelude.sail3
1 files changed, 1 insertions, 2 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 21fcbe92..7bf0d9f9 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -2,9 +2,8 @@ default Order dec
$include <smt.sail>
$include <arith.sail>
-// $include <trace.sail>
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool