English
Cons prepends an element a of α to a vector of length n, producing a vector of length n+1.
Русский
Опреление добавляет элемент a в начало вектора длины n, получая вектор длины n+1.
LaTeX
$$$\\mathrm{cons} : \\alpha \\to \\text{Vector } \\alpha n \\to \\text{Vector } \\alpha (n+1)$ with $\\mathrm{cons}(a, \\langle v, h \\rangle) = \\langle a :: v, \\mathrm{congrArg} \\; Nat.succ h \\rangle$$$
Lean4
/-- If `a : α` and `l : Vector α n`, then `cons a l`, is the vector of length `n + 1`
whose first element is a and with l as the rest of the list. -/
@[match_pattern]
def cons : α → Vector α n → Vector α (Nat.succ n)
| a, ⟨v, h⟩ => ⟨a :: v, congrArg Nat.succ h⟩
