summaryrefslogtreecommitdiff
path: root/test/mono/assert2.sail
diff options
context:
space:
mode:
Diffstat (limited to 'test/mono/assert2.sail')
-rw-r--r--test/mono/assert2.sail22
1 files changed, 22 insertions, 0 deletions
diff --git a/test/mono/assert2.sail b/test/mono/assert2.sail
index 67e18f76..edf92710 100644
--- a/test/mono/assert2.sail
+++ b/test/mono/assert2.sail
@@ -1,3 +1,17 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+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}
+
+/* Should find a set constraint below the let */
+
val f : forall 'n. atom('n) -> unit effect {escape}
function f(n) = {
@@ -7,3 +21,11 @@ function f(n) = {
()
}
}
+
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ f(8);
+ f(16);
+} \ No newline at end of file