structure Lean.Grind.Config : Type

The configuration for grind. Passed to grind using, for example, the grind (config := { eager := true }) syntax.

• eager : Bool

  When eager is true (default: false), grind eagerly splits if-then-else and match expressions during internalization.

• splits : Nat

  Maximum number of branches (i.e., case-splits) in the proof search tree.

• ematch : Nat

  Maximum number of E-matching (aka heuristic theorem instantiation) in a proof search tree branch.

• gen : Nat

  Maximum term generation. The input goal terms have generation 0. When we instantiate a theorem using a term from generation n, the new terms have generation n+1. Thus, this parameter limits the length of an instantiation chain.

• instances : Nat

  Maximum number of theorem instances generated using E-matching in a proof search tree branch.

instance Lean.Grind.instInhabitedConfig : Inhabited Lean.Grind.Config

Equations

• Lean.Grind.instInhabitedConfig = { default := { eager := default, splits := default, ematch := default, gen := default, instances := default } }

instance Lean.Grind.instBEqConfig : BEq Lean.Grind.Config

Equations

• Lean.Grind.instBEqConfig = { beq := Lean.Grind.beqConfig✝ }

grind tactic and related tactics.

def Lean.Parser.Tactic.grind : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.