English
Let α be a type and v a vector of length n over α. The operation cons(a, v) creates a vector of length n+1 whose first element is a and whose tail is v; equivalently, for every index i in Fin2(n+1), (cons(a,v))(fz) = a and (cons(a,v))(fs(i)) = v(i).
Русский
Пусть α — множество, v — вектор длины n над α. Операция cons(a, v) образует вектор длины n+1, первый элемент которого равен a, а хвост равен v; тождественно, для любого индекса i в Fin2(n+1): (cons(a,v))(fz) = a и (cons(a,v))(fs(i)) = v(i).
LaTeX
$$$\mathrm{cons} : \alpha \times \mathrm{Vector3}(\alpha,n) \to \mathrm{Vector3}(\alpha,n+1) \\\\ (\mathrm{cons}(a,v))(\mathrm{fz}) = a , \quad (\mathrm{cons}(a,v))(\mathrm{fs}(i)) = v(i).$$$
Lean4
/-- The vector cons operation -/
@[match_pattern]
def cons (a : α) (v : Vector3 α n) : Vector3 α (n + 1) := fun i =>
by
refine i.cases' ?_ ?_
· exact a
· exact v
