English
RestrictVar removes unused variables from a term, by re-mapping only the variables in a chosen finite set to a new set; the resulting term uses only the target variables.
Русский
RestrictVar удаляет неиспользуемые переменные из терма, сопоставляя новые переменные только тем переменным, которые входят в заданный набор; получившийся терм использует только целевые переменные.
LaTeX
$$$ \text{restrictVar}_{L}({t},{f}) : L.\text{Term }\beta $$$
Lean4
/-- Restricts a term to use only a set of the given variables. -/
def restrictVar [DecidableEq α] : ∀ (t : L.Term α) (_f : t.varFinset → β), L.Term β
| var a, f => var (f ⟨a, mem_singleton_self a⟩)
| func F ts, f =>
func F fun i =>
(ts i).restrictVar (f ∘ Set.inclusion (subset_biUnion_of_mem (fun i => varFinset (ts i)) (mem_univ i)))
