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

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