English
For any α and n, the function converting a fixed-length vector to a list is primitive recursive.
Русский
Для любых типа α и длины n функция преобразования вектора фиксированной длины к списку является примитивно-рекурсивной.
LaTeX
$$$$ \\operatorname{Primrec}\\big( \\mathrm{List.Vector.toList} : \\mathrm{List.Vector}\\ \\alpha\\ n \\to \\mathrm{List}\\ \\alpha \\big). $$$$
Lean4
theorem vector_toList {n} : Primrec (@List.Vector.toList α n) :=
subtype_val