English
Given α, α' : TypeVec n and β, β' : Type, the operation appendFun f g creates an arrow from append1 α β to append1 α' β' by applying f on the prefix and g on the last coordinate.
Русский
Пусть α, α' : TypeVec n и β, β' : Type. Операция appendFun f g создаёт стрелу от append1 α β к append1 α' β', применяя f к префиксу и g к последней координате.
LaTeX
$$$\mathrm{appendFun} : (\alpha \Rightarrow \alpha') \to (\beta \to \beta') \to (\alpha \append1 \beta) \Rightarrow (\alpha' \append1 \beta')$$$
Lean4
/-- append an arrow and a function as well as their respective source and target types / typevecs -/
def appendFun {α α' : TypeVec n} {β β' : Type*} (f : α ⟹ α') (g : β → β') : append1 α β ⟹ append1 α' β' :=
splitFun f g
