Documentation

Lean.Meta.Match.MVarRenaming

structure Lean.Meta.MVarRenaming :

Type

map : Lean.MVarIdMap Lean.MVarId

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

Equations

Lean.Meta.MVarRenaming.isEmpty s = Std.RBMap.isEmpty s.map

def Lean.Meta.MVarRenaming.find? (s : Lean.Meta.MVarRenaming) (mvarId : Lean.MVarId) :

Option Lean.MVarId

Equations

Lean.Meta.MVarRenaming.find? s mvarId = Std.RBMap.find? s.map mvarId

def Lean.Meta.MVarRenaming.find! (s : Lean.Meta.MVarRenaming) (mvarId : Lean.MVarId) :

Equations

Lean.Meta.MVarRenaming.find! s mvarId = Option.get! (Lean.Meta.MVarRenaming.find? s mvarId)

def Lean.Meta.MVarRenaming.insert (s : Lean.Meta.MVarRenaming) (mvarId : Lean.MVarId) (mvarId' : Lean.MVarId) :

Lean.Meta.MVarRenaming

Equations

Lean.Meta.MVarRenaming.insert s mvarId mvarId' = { map := Std.RBMap.insert s.map mvarId mvarId' }

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

Equations

Lean.Meta.MVarRenaming.apply s e = if (!Lean.Expr.hasMVar e) = true then e else if Std.RBMap.isEmpty s.map = true then e else Lean.Expr.replace (fun e => match e with | Lean.Expr.mvar mvarId x => match Std.RBMap.find? s.map mvarId with | none => some e | some newMVarId => some (Lean.mkMVar newMVarId) | x => none) e