English
A vector is a pair consisting of a list and a proof that its length matches the fixed n; toList projects to the underlying list.
Русский
Вектор представляет собой пару: список и доказательство равенства длин. toList отображает вектор в этот список.
LaTeX
$$$\\mathrm{toList}(\\langle l, h \\rangle) = l$$$
Lean4
/-- `List.Vector α n` is the type of lists of length `n` with elements of type `α`.
Note that there is also `Vector α n` in the root namespace,
which is the type of *arrays* of length `n` with elements of type `α`.
Typically, if you are doing programming or verification, you will primarily use `Vector α n`,
and if you are doing mathematics, you may want to use `List.Vector α n` instead.
-/
def Vector (α : Type u) (n : ℕ) :=
{ l : List α // l.length = n }
