4 files changed, 7 insertions, 47 deletions
diff --git a/test/mono/assert.sail b/test/mono/assert.sail
index a7c148bd..6d83a0b9 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -1,15 +1,6 @@
-$include <smt.sail>
-$include <flow.sail>
-$include <arith.sail>
 default Order dec
-type bits ('n : Int) = bitvector('n, dec)
-val operator & = "and_bool" : (bool, bool) -> bool
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-overload operator == = {eq_int, eq_vec}
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-overload operator < = {lt_atom, lt_int}
+$include <prelude.sail>
+$include <smt.sail>
 
 /* Tests set constraints in different constraints */
 
diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail
index 2cd0ab9c..b1df7010 100644
--- a/test/mono/castreq.sail
+++ b/test/mono/castreq.sail
@@ -1,32 +1,14 @@
-$include <smt.sail>
-$include <flow.sail>
-$include <arith.sail>
 default Order dec
-type bits ('n : Int) = bitvector('n, dec)
-val operator & = "and_bool" : (bool, bool) -> bool
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-overload operator == = {eq_int, eq_vec}
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-overload operator < = {lt_atom, lt_int}
+$include <prelude.sail>
+$include <smt.sail>
 val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
 val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
 function extzv(m, v) = extz_vec(m,v)
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
-  (bits('n), bits('m)) -> bits('n + 'm)
-overload append = {bitvector_concat}
 val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
 val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
 overload length = {bitvector_length}
 overload __size = {length}
-val add_bits = {ocaml: "add_vec", lem: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-overload operator + = {add_bits}
-val vector_update_subrange = {
-  ocaml: "update_subrange",
-  lem: "update_subrange_vec_dec"
-} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
 
 /* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */
diff --git a/test/mono/test_extra.lem b/test/mono/test_extra.lem
index 29876223..2dc8dd13 100644
--- a/test/mono/test_extra.lem
+++ b/test/mono/test_extra.lem
@@ -6,6 +6,7 @@ open import Sail2_prompt_monad
 open import Sail2_state
 
 let undefined_int () = return (0:ii)
+let undefined_unit () = return ()
 val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e
 let undefined_bitvector len = return (of_bools (repeat [false] len))
 
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail
index 1deb571f..fa8bcb20 100644
--- a/test/mono/times8div8.sail
+++ b/test/mono/times8div8.sail
@@ -1,24 +1,10 @@
-$include <smt.sail>
-$include <flow.sail>
-$include <arith.sail>
 default Order dec
-type bits ('n : Int) = bitvector('n, dec)
-val operator & = "and_bool" : (bool, bool) -> bool
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-overload operator == = {eq_int, eq_vec}
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-overload operator < = {lt_atom, lt_int}
+$include <prelude.sail>
+$include <smt.sail>
 val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure
 val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
 function extzv(m,v) = extz_vec(m,v)
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int).
-  (bits('n), bits('m)) -> bits('n + 'm)
-overload append = {bitvector_concat}
 val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
-val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
-overload length = {bitvector_length}
 val cast ex_int : int -> {'n, true. atom('n)}
 function ex_int 'n = n
 val quotient = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (int, int) -> int