TorchLean API
Docs Home
Guide
Examples
Graphs
Lean
.
Elab
.
Tactic
.
RenameInaccessibles
Search
Declaration colors
def
theorem
structure
axiom
return to top
source
Imports
Lean.Elab.Binders
Lean.Elab.Term
Imported by
Lean
.
Elab
.
Tactic
.
renameInaccessibles
source
def
Lean
.
Elab
.
Tactic
.
renameInaccessibles
(
mvarId
:
MVarId
)
(
hs
:
TSyntaxArray
`Lean.binderIdent
)
:
TermElabM
MVarId
Instances For