Documentation
Lean
.
Elab
.
Tactic
.
Grind
.
BuiltinTactic
Search
return to top
source
Imports
Lean.Elab.SetOption
Lean.Elab.Tactic.Basic
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.Filter
Lean.Elab.Tactic.Grind.Param
Lean.Elab.Tactic.Grind.ShowState
Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Tactic.Grind.EMatchTheorem
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
Equations
Instances For