Add wrappers around Lem operators using bitvector type class

Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.

1 files changed, 4 insertions, 4 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 370f9370..754a5cec 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -90,9 +90,9 @@ overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
 val and_bool = "and_bool" : (bool, bool) -> bool
 
-val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
@@ -100,9 +100,9 @@ overload operator & = {and_bool, and_vec}
 
 val or_bool = "or_bool" : (bool, bool) -> bool
 
-val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function or_vec (xs, ys) = builtin_or_vec(xs, ys)