English
Let α, α' be type vectors of length n+1. Given a prefix arrow f : drop α ⟹ drop α' and a last-coordinate arrow g : last α → last α', the map splitFun f g constructs a full arrow α ⟹ α' by acting as f on the first n coordinates and as g on the last coordinate.
Русский
Пусть α, α' — векторы типов длины n+1. Даны префиксная стрелa f : drop α ⟹ drop α' и стрелa последней координаты g : last α → last α'. Функция splitFun f g строит стрелу α ⟹ α' так, что на первых n координатах действует f, а на последней координате — g.
LaTeX
$$$\mathrm{splitFun} : (\mathrm{drop}\alpha \Rightarrow \mathrm{drop}\alpha') \to (\mathrm{last}\alpha \to \mathrm{last}\alpha') \to \alpha \Rightarrow \alpha'$$$
Lean4
/-- append an arrow and a function for arbitrary source and target type vectors -/
def splitFun {α α' : TypeVec (n + 1)} (f : drop α ⟹ drop α') (g : last α → last α') : α ⟹ α'
| Fin2.fs i => f i
| Fin2.fz => g
