TorchLean API
Docs Home
Guide
Examples
Graphs
Lean
.
Elab
.
Tactic
.
Grind
.
BuiltinTactic
Search
Declaration colors
def
theorem
structure
axiom
return to top
source
Imports
Lean.Elab.Tactic.RenameInaccessibles
Lean.Meta.Tactic.ExposeNames
Lean.Meta.Tactic.TryThis
Lean.Elab.Tactic.Grind.Anchor
Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.Grind.Param
Lean.Elab.Tactic.Grind.ShowState
Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Tactic.Grind.Internalize
Lean.Meta.Tactic.Grind.Intro
Lean.Meta.Tactic.Grind.PP
Lean.Meta.Tactic.Grind.Solve
Lean.Meta.Tactic.Grind.Split
Lean.Meta.Tactic.Grind.AC.Eq
Lean.Meta.Tactic.Grind.AC.PP
Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
Lean.Meta.Tactic.Grind.Arith.CommRing.PP
Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
Lean.Meta.Tactic.Grind.Arith.Linear.PP
Lean.Meta.Tactic.Grind.Arith.Linear.Search
Imported by
Lean
.
Elab
.
Tactic
.
Grind
.
renameInaccessibles
source
def
Lean
.
Elab
.
Tactic
.
Grind
.
renameInaccessibles
(
mvarId
:
MVarId
)
(
hs
:
TSyntaxArray
`Lean.binderIdent
)
:
GrindTacticM
MVarId
Instances For