diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/vector_access.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/vector_append.sail | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail index 9346f5fe..c7c1b502 100644 --- a/test/typecheck/pass/vector_access.sail +++ b/test/typecheck/pass/vector_access.sail @@ -1,5 +1,6 @@ -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc default Order inc diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index d2f1ca47..af83c44d 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,5 +1,4 @@ -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append @@ -10,8 +9,6 @@ val (bit[4], bit[4]) -> bit[8] effect pure test function bit[8] test (v1, v2) = { - z := vector_access(v1, 3); - z := v1[0]; zv := vector_append(v1, v2); zv := v1 : v2; zv |