diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/vector_dec.sail | 2 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 8abcd218..7011a55c 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -63,7 +63,7 @@ val bitvector_access = { lem: "access_vec_dec", coq: "access_vec_dec", c: "vector_access" -} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit +} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit val plain_vector_access = { ocaml: "access", diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index b295c92c..042a6324 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -61,7 +61,7 @@ val bitvector_access = { lem: "access_vec_inc", coq: "access_vec_inc", c: "vector_access" -} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit +} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit val plain_vector_access = { ocaml: "access", |