English
There is a canonical concatenation operation on vectors: given v1 of length n and v2 of length m, the concatenation is a vector of length n+m whose underlying list is the concatenation of the two lists.
Русский
Существует каноничное объединение двух векторов: вектор длины n и вектор длины m образуют вектор длины n+m, чья подлежащая к списку последовательность — это конкатенация двух списков.
LaTeX
$$$\\text{instance } \\{n\\; m : \\mathbb{N}\\} : \\text{HAppend } (\\text{Vector } \\alpha n) (\\text{Vector } \\alpha m) (\\text{Vector } \\alpha (n+m))$ where $\\mathrm{hAppend}(\\langle l_1,h_1\\rangle,\\langle l_2,h_2\\rangle)=\\langle l_1++l_2,\\; \\text{proof} \\rangle$$$
Lean4
instance {n m : Nat} : HAppend (Vector α n) (Vector α m) (Vector α (n + m)) where
hAppend
| ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, by simp [*]⟩
