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
    • s.isEmpty = s.map.isEmpty
    Instances For
      Equations
      Instances For

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

        Equations
        • s.insert fvarId v = if s.contains fvarId = true then s else let map := Lean.AssocList.mapVal (fun (e : Lean.Expr) => e.replaceFVarId fvarId v) s.map; { map := map.insert fvarId v }
        Instances For
          Equations
          Instances For
            Equations
            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
                  Equations
                  Instances For

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

                    Equations
                    Instances For
                      @[reducible, inline]
                      Equations
                      Instances For