Documentation

Lean.Meta.Tactic.FVarSubst

structure Lean.Meta.FVarSubst :

Type

map : Std.AssocList Lean.FVarId Lean.Expr

instance Lean.Meta.instInhabitedFVarSubst :

Inhabited Lean.Meta.FVarSubst

Equations

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

def Lean.Meta.FVarSubst.empty :

Lean.Meta.FVarSubst

Equations

Lean.Meta.FVarSubst.empty = { map := ∅ }

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

Equations

Lean.Meta.FVarSubst.isEmpty s = Std.AssocList.isEmpty s.map

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

Equations

Lean.Meta.FVarSubst.contains s fvarId = Std.AssocList.contains fvarId s.map

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

Lean.Meta.FVarSubst

Equations

Lean.Meta.FVarSubst.insert s fvarId v = if Lean.Meta.FVarSubst.contains s fvarId = true then s else let map := Std.AssocList.mapVal (fun e => Lean.Expr.replaceFVarId e fvarId v) s.map; { map := Std.AssocList.insert map fvarId v }

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

Lean.Meta.FVarSubst

Equations

Lean.Meta.FVarSubst.erase s fvarId = { map := Std.AssocList.erase fvarId s.map }

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

Option Lean.Expr

Equations

Lean.Meta.FVarSubst.find? s fvarId = Std.AssocList.find? fvarId s.map

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

Equations

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

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

Equations

Lean.Meta.FVarSubst.apply s e = if Std.AssocList.isEmpty s.map = true then e else if (!Lean.Expr.hasFVar e) = true then e else Lean.Expr.replace (fun e => match e with | Lean.Expr.fvar fvarId x => match Std.AssocList.find? fvarId s.map with | none => some e | some v => some v | x => none) e

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

List Lean.FVarId

Equations

Lean.Meta.FVarSubst.domain s = Std.AssocList.foldl (fun r k v => k :: r) [] s.map

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

Equations

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

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

Lean.LocalDecl → Lean.LocalDecl

Equations

Lean.LocalDecl.applyFVarSubst s x = match x with | Lean.LocalDecl.cdecl i id n t bi => Lean.LocalDecl.cdecl i id n (Lean.Meta.FVarSubst.apply s t) bi | Lean.LocalDecl.ldecl i id n t v nd => Lean.LocalDecl.ldecl i id n (Lean.Meta.FVarSubst.apply s t) (Lean.Meta.FVarSubst.apply s v) nd

@[inline]

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

Equations

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