English
Let m, n be natural numbers and o = m + n. For any type α, given a vector u of length m and a vector v of length n, vecAppend ho u v produces a vector of length o that is obtained by concatenating u and v. The construction depends on ho, a witness of o = m + n, ensuring the resulting vector has the correct length.
Русский
Пусть m, n — натуральные числа и o = m + n. Пусть α — множество. Даны вектор u длины m и вектор v длины n. vecAppend ho u v даёт вектор длины o, получаемый конкатенацией u и v; конструкция зависит от ho, очевидно обеспечивая корректную длину итогового вектора.
LaTeX
$$$\\operatorname{vecAppend}(ho,u,v) = (\\operatorname{Fin.append} u v) \\circ (\\operatorname{Fin.cast} ho)$$$
Lean4
/-- `vecAppend ho u v` appends two vectors of lengths `m` and `n` to produce
one of length `o = m + n`. This is a variant of `Fin.append` with an additional `ho` argument,
which provides control of definitional equality for the vector length.
This turns out to be helpful when providing simp lemmas to reduce `![a, b, c] n`, and also means
that `vecAppend ho u v 0` is valid. `Fin.append u v 0` is not valid in this case because there is
no `Zero (Fin (m + n))` instance. -/
def vecAppend {α : Type*} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) : Fin o → α :=
Fin.append u v ∘ Fin.cast ho
