English
Specialized destructor on WPath: given a family g' on the tail and a family g on children, define a function that destructs WPath ⟨a,f⟩ by case-splitting on the WPath structure.
Русский
Специализированная деконструкция на WPath: задана пара семейств g' и g, формирующая разложение WPath ⟨a,f⟩ по образцу структуры.
LaTeX
$$$\def wPathCasesOn {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a ⟹ α) (g : ∀ j : P.last.B a, P.WPath (f j) ⟹ α) : P.WPath ⟨a, f⟩ ⟹ α$$$
Lean4
/-- Specialized destructor on `WPath` -/
def wPathCasesOn {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a ⟹ α)
(g : ∀ j : P.last.B a, P.WPath (f j) ⟹ α) : P.WPath ⟨a, f⟩ ⟹ α :=
by
intro i x
match x with
| WPath.root _ _ i c => exact g' i c
| WPath.child _ _ i j c => exact g j i c
