def Lean.Grind.grindLintCheck : ParserDescr

#grind_lint check analyzes all theorems annotated for theorem instantiation using E-matching.

It creates artificial goals and reports the number of instances each theorem produces. The command helps detect long or unbounded theorem instantiation chains.

Usage examples:

#grind_lint check
#grind_lint check (min:=10) (detailed:=50)
#grind_lint check in Foo Bar -- restrict analysis to these namespaces
#grind_lint check in module Foo -- restrict analysis to theorems defined in module `Foo` or any of its submodules

Options can include any valid grind configuration option, and min and detailed.

• min: minimum number of instantiations to print a summary (default: 10)
• detailed: minimum number of instantiations to print detailed breakdown (default: 50) If the option trace.grind.* is enabled, additional details are printed.

By default, #grind_lint uses the following grind configuration:

  splits       := 0
  lookahead    := false
  mbtc         := false
  ematch       := 20
  instances    := 100
  gen          := 10

Consider using #grind_lint inspect <thm> to focus on specific theorems.

Equations

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

def Lean.Grind.grindLintInspect : ParserDescr

#grind_lint inspect thm₁ … analyzes the specified theorem(s) individually.

It always prints detailed statistics regardless of thresholds and is useful for investigating specific grind lemmas that may generate excessive instantiations. Examples:

#grind_lint inspect Array.zip_map

You can use set_option trace.grind.ematch.instance true to instruct grind to display the actual instances it produces.

Equations

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

def Lean.Grind.grindLintMute : ParserDescr

#grind_lint mute thm₁ … marks the given theorem(s) as muted during linting.

Muted theorems remain in the environment but are not instantiated when running #grind_lint check or #grind_lint inspect. This is useful for suppressing noisy or recursive lemmas that cause excessive E-matching without removing their annotations.

Example:

#grind_lint mute Array.zip_map Int.zero_shiftRight

Equations

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

def Lean.Grind.grindLintSkip : ParserDescr

#grind_lint skip thm₁ … marks the given theorem(s) to be skipped entirely by #grind_lint check. Skipped theorems are neither analyzed nor reported, but may still be used for instantiation when analyzing other theorems. Example:

#grind_lint skip Array.range_succ

Equations

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