English
Define a motive on Vector α n by case analysis on v : Vector α n, using nil for the nil case and cons to build from heads hd with tail tl. Then motive v is obtained by applying inductionOn with that nil and cons.
Русский
Задаём рассуждение по вектору α n через разбор случаев: nil задаёт базовый случай, cons — переход к вектору с головой hd и хвостом tl. Тогда мотива для произвольного v получается через индукцию(inductionOn).
LaTeX
$$$\\text{casesOn}\\{motive\\} (v : Vector α n) (nil) (cons) = \\text{inductionOn} (C := motive) v nil @\\tfrac{_}{_} \\;⇒\\; motive v$$$
Lean4
/-- Define `motive v` by case-analysis on `v : Vector α n`. -/
def casesOn {motive : ∀ {n}, Vector α n → Sort*} (v : Vector α m) (nil : motive nil)
(cons : ∀ {n}, (hd : α) → (tl : Vector α n) → motive (Vector.cons hd tl)) : motive v :=
inductionOn (C := motive) v nil @fun _ hd tl _ => cons hd tl
