diff options
Diffstat (limited to 'test/mono/times8div8.sail')
| -rw-r--r-- | test/mono/times8div8.sail | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail index 31f63fda..a5fd1c37 100644 --- a/test/mono/times8div8.sail +++ b/test/mono/times8div8.sail @@ -1,5 +1,6 @@ $include <smt.sail> $include <flow.sail> +$include <arith.sail> default Order dec type bits ('n : Int) = vector('n, dec, bit) val operator & = "and_bool" : (bool, bool) -> bool @@ -10,8 +11,8 @@ 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} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) 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} |