diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/exist_pattern.sail | 4 | ||||
| -rw-r--r-- | test/typecheck/pass/nondet_assert.sail | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 46913de4..4561074a 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -4,6 +4,10 @@ register nat n register nat x register nat y +val (int, int) -> bool effect pure eq_int + +overload (deinfix ==) [eq_int] + typedef wordsize = exist 'n, 'n IN {8,16,32}. [|'n|] let (wordsize) word = ([|8|]) 8 diff --git a/test/typecheck/pass/nondet_assert.sail b/test/typecheck/pass/nondet_assert.sail index e90bb6f2..501432d3 100644 --- a/test/typecheck/pass/nondet_assert.sail +++ b/test/typecheck/pass/nondet_assert.sail @@ -1,7 +1,7 @@ register int z -val unit -> int effect {wreg, rreg} test +val unit -> int effect {wreg, rreg, escape} test function int test () = { nondet { |