diff options
Diffstat (limited to 'test/mono/assert2.sail')
| -rw-r--r-- | test/mono/assert2.sail | 22 |
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 |
