vector_length — Mathlib

English

The length of a fixed-length vector is a constant primitive recursive function.

Русский

Длина вектора фиксированной длины является константной примитивно-рекурсивной функцией.

LaTeX

$$$$ \\operatorname{Primrec}\\big( \\mathrm{List.Vector.length} : \\mathrm{List.Vector}\\ \\alpha\\ n \\to \\mathbb{N} \\big). $$$$

Lean4

theorem vector_length {n} : Primrec (@List.Vector.length α n) :=
  const _

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