blob: 6ff4f9f61bc1c96a0239688d3c0aafcf1c268f03 (
plain)
1
2
3
4
5
6
|
val vector_update_subrange = {
ocaml: "update_subrange",
lem: "update_subrange_vec_dec",
c: "vector_update_subrange",
coq: "update_subrange_vec_dec"
} : forall 'n 'm 'o. (#\hyperref[zbits]{bits}#('n), atom('m), atom('o), #\hyperref[zbits]{bits}#('m - ('o - 1))) -> #\hyperref[zbits]{bits}#('n)
|
