source
structure Lean.Meta.MVarRenaming :
Type

A mapping from MVarId to MVarId

- map : MVarIdMap MVarId

Instances For

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

- s.isEmpty = Std.TreeMap.isEmpty s.map

Instances For

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

- s.find? mvarId = Std.TreeMap.get? s.map mvarId

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For