English
RecOn gives a recursion principle where the vector is the primary argument: for every C, and base H0 and step Hs, one gets a function that computes C on any Vector3 α n.
Русский
Рекурсия с вектором в качестве главного аргумента: для любого C и базового H0 и шага Hs существует функция, вычисляющая C на любом Vector3 α n.
LaTeX
$$$ {\mathrm{recOn}}_{C}(v)(H0,Hs) = \begin{cases} H0 & v = [], \\ Hs(a,t)(v.recOn(H0,Hs)) & v = a :: t. \end{cases} $$$
Lean4
/-- Recursion principle with the vector as first argument. -/
@[elab_as_elim]
protected def recOn {C : ∀ {n}, Vector3 α n → Sort u} {n} (v : Vector3 α n) (H0 : C [])
(Hs : ∀ {n} (a) (w : Vector3 α n), C w → C (a :: w)) : C v :=
match n with
| 0 => v.nilElim H0
| _ + 1 => v.consElim fun a t => Hs a t (Vector3.recOn t H0 Hs)
