Documentation
Lean
.
Elab
.
Tactic
.
Grind
.
ShowState
Search
return to top
source
Imports
Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Filter
Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Tactic.Grind.EMatchTheoremParam
Lean.Meta.Tactic.Grind.PP
Lean.Meta.Tactic.Grind.Split
Imported by
Lean
.
Elab
.
Tactic
.
Grind
.
showState
source
def
Lean
.
Elab
.
Tactic
.
Grind
.
showState
(
filter
:
Meta.Grind.Filter
)
(
isSilent
:
Bool
:=
false
)
:
GrindTacticM
Unit
Equations
Instances For