Documentation
Lean
.
Meta
.
Tactic
.
Grind
Search
return to top
source
Imports
Lean.Meta.Tactic.Grind.Arith
Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Tactic.Grind.Canon
Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Tactic.Grind.CasesMatch
Lean.Meta.Tactic.Grind.Core
Lean.Meta.Tactic.Grind.Ctor
Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Tactic.Grind.Ext
Lean.Meta.Tactic.Grind.Injection
Lean.Meta.Tactic.Grind.Inv
Lean.Meta.Tactic.Grind.Main
Lean.Meta.Tactic.Grind.MarkNestedProofs
Lean.Meta.Tactic.Grind.MatchCond
Lean.Meta.Tactic.Grind.MatchDiscrOnly
Lean.Meta.Tactic.Grind.PP
Lean.Meta.Tactic.Grind.Parser
Lean.Meta.Tactic.Grind.Proof
Lean.Meta.Tactic.Grind.Propagate
Lean.Meta.Tactic.Grind.RevertAll
Lean.Meta.Tactic.Grind.Simp
Lean.Meta.Tactic.Grind.Types
Lean.Meta.Tactic.Grind.Util
Imported by
Trace options for
grind
users
Trace options for
grind
developers