Documentation
Lean
.
Meta
.
Match
.
MVarRenaming
Search
return to top
source
Imports
Lean.Util.ReplaceExpr
Imported by
Lean.Meta.Match.Match
Lean
.
Meta
.
MVarRenaming
Lean
.
Meta
.
MVarRenaming
.
isEmpty
Lean
.
Meta
.
MVarRenaming
.
find?
Lean
.
Meta
.
MVarRenaming
.
find!
Lean
.
Meta
.
MVarRenaming
.
insert
Lean
.
Meta
.
MVarRenaming
.
apply
source
structure
Lean
.
Meta
.
MVarRenaming
:
Type
A mapping from MVarId to MVarId
map :
MVarIdMap
MVarId
source
def
Lean
.
Meta
.
MVarRenaming
.
isEmpty
(
s
:
MVarRenaming
)
:
Bool
Equations
s
.
isEmpty
=
Lean.RBMap.isEmpty
s
.
map
source
def
Lean
.
Meta
.
MVarRenaming
.
find?
(
s
:
MVarRenaming
)
(
mvarId
:
MVarId
)
:
Option
MVarId
Equations
s
.
find?
mvarId
=
Lean.RBMap.find?
s
.
map
mvarId
source
def
Lean
.
Meta
.
MVarRenaming
.
find!
(
s
:
MVarRenaming
)
(
mvarId
:
MVarId
)
:
MVarId
Equations
s
.
find!
mvarId
=
(
s
.
find?
mvarId
)
.
get!
source
def
Lean
.
Meta
.
MVarRenaming
.
insert
(
s
:
MVarRenaming
)
(
mvarId
mvarId'
:
MVarId
)
:
MVarRenaming
Equations
s
.
insert
mvarId
mvarId'
=
{
map
:=
s
.
map
.
insert
mvarId
mvarId'
}
source
def
Lean
.
Meta
.
MVarRenaming
.
apply
(
s
:
MVarRenaming
)
(
e
:
Expr
)
:
Expr
Equations
One or more equations did not get rendered due to their size.