summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorThomas Bauereiss2017-09-13 19:03:31 +0100
committerThomas Bauereiss2017-09-14 13:11:44 +0100
commitcb90735550541fa6752aaad82ff809d84e6c5f88 (patch)
treef1b90dc759efa73e626eafeed8a239a0105e9ccd /lib
parent3914be09d200eb92ed1e317123f56667d597b5a7 (diff)
Fix some more test cases
Diffstat (limited to 'lib')
-rw-r--r--lib/prelude_wrappers.sail4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/prelude_wrappers.sail b/lib/prelude_wrappers.sail
index 4568f6ab..1d85b4ff 100644
--- a/lib/prelude_wrappers.sail
+++ b/lib/prelude_wrappers.sail
@@ -1,5 +1,5 @@
-val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
-val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,inc,bit> effect pure to_vec_inc
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec
+val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,inc,bit> effect pure to_vec_inc
function forall Num 'n, Num 'm. (vector<'m - 1,'m,dec,bit>) to_vec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n)
function forall Num 'm. (vector<'m - 1,'m,dec,bit>) to_svec (n) = to_vec_dec ((sizeof 'm) - 1, sizeof 'm, n)