cheri/sail_latexcc/sailccvectorlength.tex


1
2
3
4
5
6

val vector_length = {
  ocaml: "length",
  lem: "length_list",
  c: "length",
  coq: "vec_length"
} : forall '#\hyperref[zn]{n}# ('a : Type). vector('n, dec, 'a) -> atom('n)