Documentation

Lean.Meta.Tactic.Grind

Imports

Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Tactic.Grind.Canon
Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Tactic.Grind.Core
Lean.Meta.Tactic.Grind.Ctor
Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Tactic.Grind.Injection
Lean.Meta.Tactic.Grind.Inv
Lean.Meta.Tactic.Grind.Main
Lean.Meta.Tactic.Grind.MarkNestedProofs
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