structure Lean.Meta.MVarRenaming : Type

A mapping from MVarId to MVarId

• map : MVarIdMap MVarId

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

Equations

• s.isEmpty = Lean.RBMap.isEmpty s.map

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

Equations

• s.find? mvarId = Lean.RBMap.find? s.map mvarId

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

Equations

• s.find! mvarId = (s.find? mvarId).get!

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

Equations

• s.insert mvarId mvarId' = { map := s.map.insert mvarId mvarId' }

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

Equations

• One or more equations did not get rendered due to their size.