diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/exist_pattern.sail | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 96b1ecf1..c701f12b 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -1,6 +1,6 @@ default Order inc -infix 4 == +$include <prelude.sail> register n : nat @@ -8,16 +8,6 @@ register x : nat register y : nat -val eq_int = {lem: "eq", coq: "Z.eqb"} : (int, int) -> bool -val eq_vec = {lem: "eq_vec", coq: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool - -overload operator == = {eq_int, eq_vec} - -val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool - -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc", coq: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. - (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit) - type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)} let word : wordsize = 8 : range(0, 8) |