English
There is a deprecated function append that concatenates two vectors, producing a vector of length n+m with underlying list l1 ++ l2; users are advised to use the standard ++ operator instead.
Русский
Существуют устаревшие функции append, которые конкатенируют два вектора, получая вектор длины n+m с подлежащим списком l1 ++ l2; рекомендуется использовать стандартный ++.
LaTeX
$$$\\text{append} \\;\\{n\\; m\\} : \\text{Vector } \\alpha n \\to \\text{Vector } \\alpha m \\to \\text{Vector } \\alpha (n+m)$ with $\\mathrm{append}(\\langle l_1,h_1\\rangle)(\\langle l_2,h_2\\rangle) = \\langle l_1 ++ l_2, \\text{proof} \\rangle$$$
Lean4
/-- Appending a vector to another. -/
@[deprecated "use `++` instead" (since := "2025-06-05")]
def append {n m : Nat} : Vector α n → Vector α m → Vector α (n + m)
| ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, by simp [*]⟩
