diff options
Diffstat (limited to 'test/typecheck')
| -rw-r--r-- | test/typecheck/pass/sizeof_vector_start_index.sail | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/typecheck/pass/sizeof_vector_start_index.sail b/test/typecheck/pass/sizeof_vector_start_index.sail new file mode 100644 index 00000000..6ad8ef06 --- /dev/null +++ b/test/typecheck/pass/sizeof_vector_start_index.sail @@ -0,0 +1,12 @@ +val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'n:] effect pure vector_start_index + +function forall Num 'n, Num 'm, Order 'ord, Type 'a. [:'n:] vector_start_index ((vector<'n,'m,'ord,'a>) vec) = +{ + sizeof 'n +} + +function int test ((vector<47,11,dec,bit>) vec) = +{ + vector_start_index(vec) +} + |