English
Substituting the function symbols in a term by expressions yields a new term in a target language, by recursively substituting inside the subterms.
Русский
Подстановка функций в терм заменяет символы функций на выражения и получает новый терм в целевом языке, рекурсивно подменяя вложенные термы.
LaTeX
$$$\\mathrm{substFunc}: L.T erm(\\alpha) \\to (∀{n}, L.Functions n \\to L'.Term(\\mathrm{Fin}\\ n)) \\to L'.Term(\\alpha)$ defined by structural recursion on the term.$$
Lean4
/-- Substitutes the functions in a given term with expressions. -/
@[simp]
def substFunc : L.Term α → (∀ {n : ℕ}, L.Functions n → L'.Term (Fin n)) → L'.Term α
| var a, _ => var a
| func f ts, tf => (tf f).subst fun i ↦ (ts i).substFunc tf
