structure Lean.Meta.FVarSubst : Type

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.

• map : AssocList FVarId Expr

instance Lean.Meta.instInhabitedFVarSubst : Inhabited FVarSubst

def Lean.Meta.FVarSubst.empty : FVarSubst

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

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

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

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

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

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

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

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

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

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

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

def Lean.Meta.FVarSubst.append (s t : FVarSubst) : FVarSubst

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

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

@[reducible, inline]

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