cheri/sail_latexcc/sailccbitvectoraccess.tex


1
2
3
4
5
6

val bitvector_access = {
  ocaml: "access",
  lem: "access_vec_dec",
  coq: "access_vec_dec",
  c: "vector_access"
} : forall ('n : Int), 'n >= 0. (#\hyperref[zbits]{bits}#('n), int) -> bit