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.

Instances For

• Lean.Grind.instBEqConfig
• Lean.Grind.instInhabitedConfig

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

Equations

• Lean.Grind.instInhabitedConfig = { default := { eager := default } }

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

Equations

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

grind tactic and related tactics.