structure Lean.Meta.FVarSubst : Type

• map : Lean.AssocList Lean.FVarId Lean.Expr

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.

instance Lean.Meta.instInhabitedFVarSubst : Inhabited Lean.Meta.FVarSubst

def Lean.Meta.FVarSubst.empty : Lean.Meta.FVarSubst

def Lean.Meta.FVarSubst.isEmpty (s : Lean.Meta.FVarSubst) : Bool

def Lean.Meta.FVarSubst.contains (s : Lean.Meta.FVarSubst) (fvarId : Lean.FVarId) : Bool

def Lean.Meta.FVarSubst.insert (s : Lean.Meta.FVarSubst) (fvarId : Lean.FVarId) (v : Lean.Expr) : Lean.Meta.FVarSubst

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

def Lean.Meta.FVarSubst.erase (s : Lean.Meta.FVarSubst) (fvarId : Lean.FVarId) : Lean.Meta.FVarSubst

def Lean.Meta.FVarSubst.find? (s : Lean.Meta.FVarSubst) (fvarId : Lean.FVarId) : Option Lean.Expr

def Lean.Meta.FVarSubst.get (s : Lean.Meta.FVarSubst) (fvarId : Lean.FVarId) : Lean.Expr

def Lean.Meta.FVarSubst.apply (s : Lean.Meta.FVarSubst) (e : Lean.Expr) : Lean.Expr

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

def Lean.Meta.FVarSubst.domain (s : Lean.Meta.FVarSubst) : List Lean.FVarId

def Lean.Meta.FVarSubst.any (p : Lean.FVarId → Lean.Expr → Bool) (s : Lean.Meta.FVarSubst) : Bool

def Lean.LocalDecl.applyFVarSubst (s : Lean.Meta.FVarSubst) : Lean.LocalDecl → Lean.LocalDecl

@[inline, reducible]

abbrev Lean.Expr.applyFVarSubst (s : Lean.Meta.FVarSubst) (e : Lean.Expr) : Lean.Expr