English
The operation that prepends an element to a vector is primitive recursive (binary operation on vectors).
Русский
Операция добавления элемента в начале вектора является примитивно-рекурсивной (бинарная операция над векторами).
LaTeX
$$$$ \\operatorname{Primrec}_2\\big( \\mathrm{List.Vector.cons}\\ \\alpha\\ n \\big). $$$$
Lean4
theorem vector_cons {n} : Primrec₂ (@List.Vector.cons α n) :=
vector_toList_iff.1 <| by simpa using list_cons.comp fst (vector_toList_iff.2 snd)