Documentation

Lean.Meta.Tactic.FVarSubst

structure Lean.Meta.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.

map : AssocList FVarId Expr

Instances For

Lean.Meta.instInhabitedFVarSubst

instance Lean.Meta.instInhabitedFVarSubst :

Inhabited FVarSubst

Equations

Lean.Meta.instInhabitedFVarSubst = { default := { map := default } }

def Lean.Meta.FVarSubst.empty :

Equations

Lean.Meta.FVarSubst.empty = { }

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

Equations

s.isEmpty = s.map.isEmpty

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

Equations

s.contains fvarId = Lean.AssocList.contains fvarId s.map

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

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.insertNew fvarId v }

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

Equations

s.erase fvarId = { map := Lean.AssocList.erase fvarId s.map }

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

Equations

s.find? fvarId = Lean.AssocList.find? fvarId s.map

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

Equations

s.get fvarId = match Lean.AssocList.find? fvarId s.map with | none => Lean.mkFVar fvarId | some v => v

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

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.

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

Equations

s.domain = Lean.AssocList.foldl (fun (r : List Lean.FVarId) (k : Lean.FVarId) (x : Lean.Expr) => k :: r) [] s.map

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

Equations

Lean.Meta.FVarSubst.any p s = Lean.AssocList.any p s.map

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

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

Equations

s.append t = Lean.AssocList.foldl (fun (s' : Lean.Meta.FVarSubst) (k : Lean.FVarId) (v : Lean.Expr) => s'.insert k (t.apply v)) t s.map

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

LocalDecl → LocalDecl

Equations

Lean.LocalDecl.applyFVarSubst s (Lean.LocalDecl.cdecl i id n t bi k) = Lean.LocalDecl.cdecl i id n (s.apply t) bi k
Lean.LocalDecl.applyFVarSubst s (Lean.LocalDecl.ldecl i id n t v nd k) = Lean.LocalDecl.ldecl i id n (s.apply t) (s.apply v) nd k

@[reducible, inline]

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

Equations

Lean.Expr.applyFVarSubst s e = s.apply e