cheri/sail_latexcc/sailccplainvectorupdate.tex


1
2
3
4
5
6

val plain_vector_update = {
  ocaml: "update",
  lem: "update_list_dec",
  coq: "vec_update_dec",
  c: "vector_update"
} : forall '#\hyperref[zn]{n}# ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)