blob: c069c7b6cdf86ebd6ac08e0d0eb4b8b8228f1726 (
plain)
1
2
3
4
5
6
7
|
val vector_subrange = {
ocaml: "subrange",
lem: "subrange_vec_dec",
c: "vector_subrange",
coq: "subrange_vec_dec"
} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n.
(#\hyperref[zbits]{bits}#('n), atom('m), atom('o)) -> #\hyperref[zbits]{bits}#('m - 'o + 1)
|
