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

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

    Instances For

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

      Instances For
        @[inline, reducible]
        Instances For