diff options
Diffstat (limited to 'lib/vector_dec.sail')
| -rw-r--r-- | lib/vector_dec.sail | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 86bbe601..8abcd218 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -22,7 +22,7 @@ val vector_length = { ocaml: "length", lem: "length_list", c: "length", - coq: "length_list" + coq: "vec_length" } : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) overload length = {bitvector_length, vector_length} @@ -68,7 +68,7 @@ val bitvector_access = { val plain_vector_access = { ocaml: "access", lem: "access_list_dec", - coq: "access_list_dec", + coq: "vec_access_dec", c: "vector_access" } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a @@ -84,7 +84,7 @@ val bitvector_update = { val plain_vector_update = { ocaml: "update", lem: "update_list_dec", - coq: "update_list_dec", + coq: "vec_update_dec", c: "vector_update" } : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) |