vector_toList — Mathlib

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

Похожие утверждения