# Documentation

Lean.Meta.Tactic.FVarSubst

Some tactics substitute hypotheses with expressions. We track these substitutions using FVarSubst. It is just a mapping from the original FVarId (internal) name to an expression. The free variables occurring in the expression must be defined in the new goal.

Instances For
Equations
Equations

Add entry fvarId |-> v to s if s does not contain an entry for fvarId.

Equations
• One or more equations did not get rendered due to their size.
Equations

Given e, for each (x => v) in s replace x with v in e

Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.