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.

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

        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.
        Instances For

          Constructs a substitution consisting of s followed by t. This satisfies (s.append t).apply e = t.apply (s.apply e)

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