def Lean.Parser.resetGrindAttrs : ParserDescr

Reset all grind attributes. This command is intended for testing purposes only and should not be used in applications.

Equations

• Lean.Parser.resetGrindAttrs = Lean.ParserDescr.node `Lean.Parser.resetGrindAttrs 1024 (Lean.ParserDescr.symbol "%reset_grind_attrs")

def Lean.Parser.Attr.grindEq : ParserDescr

Equations

• Lean.Parser.Attr.grindEq = Lean.ParserDescr.nodeWithAntiquot "grindEq" `Lean.Parser.Attr.grindEq (Lean.ParserDescr.symbol "= ")

def Lean.Parser.Attr.grindEqBoth : ParserDescr

Equations

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

def Lean.Parser.Attr.grindEqRhs : ParserDescr

Equations

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

def Lean.Parser.Attr.grindEqBwd : ParserDescr

Equations

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

def Lean.Parser.Attr.grindBwd : ParserDescr

Equations

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

def Lean.Parser.Attr.grindFwd : ParserDescr

Equations

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

def Lean.Parser.Attr.grindRL : ParserDescr

Equations

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

def Lean.Parser.Attr.grindLR : ParserDescr

Equations

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

def Lean.Parser.Attr.grindUsr : ParserDescr

Equations

• Lean.Parser.Attr.grindUsr = Lean.ParserDescr.nodeWithAntiquot "grindUsr" `Lean.Parser.Attr.grindUsr (Lean.ParserDescr.nonReservedSymbol "usr " false)

def Lean.Parser.Attr.grindCases : ParserDescr

Equations

• Lean.Parser.Attr.grindCases = Lean.ParserDescr.nodeWithAntiquot "grindCases" `Lean.Parser.Attr.grindCases (Lean.ParserDescr.nonReservedSymbol "cases " false)

def Lean.Parser.Attr.grindCasesEager : ParserDescr

Equations

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

def Lean.Parser.Attr.grindIntro : ParserDescr

Equations

• Lean.Parser.Attr.grindIntro = Lean.ParserDescr.nodeWithAntiquot "grindIntro" `Lean.Parser.Attr.grindIntro (Lean.ParserDescr.nonReservedSymbol "intro " false)

def Lean.Parser.Attr.grindMod : ParserDescr

Equations

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

def Lean.Parser.Attr.grind : ParserDescr

Equations

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

structure Lean.Grind.Config : Type

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

• trace : Bool

  If trace is true, grind records used E-matching theorems and case-splits.

• splits : Nat

  Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization.

• ematch : Nat

  Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split.

• 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.

• matchEqs : Bool

  If matchEqs is true, grind uses match-equations as E-matching theorems.

• splitMatch : Bool

  If splitMatch is true, grind performs case-splitting on match-expressions during the search.

• splitIte : Bool

  If splitIte is true, grind performs case-splitting on if-then-else expressions during the search.

• splitIndPred : Bool

  If splitIndPred is true, grind performs case-splitting on inductive predicates. Otherwise, it performs case-splitting only on types marked with [grind cases] attribute.

• failures : Nat

  By default, grind halts as soon as it encounters a sub-goal where no further progress can be made.

• canonHeartbeats : Nat

  Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test.

• ext : Bool

  If ext is true, grind uses extensionality theorems available in the environment.

• verbose : Bool

  If verbose is false, additional diagnostics information is not collected.

instance Lean.Grind.instInhabitedConfig : Inhabited Config

Equations

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

instance Lean.Grind.instBEqConfig : BEq Config

Equations

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

grind tactic and related tactics.

def Lean.Parser.Tactic.grindErase : ParserDescr

Equations

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

def Lean.Parser.Tactic.grindLemma : ParserDescr

Equations

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

def Lean.Parser.Tactic.grindParam : ParserDescr

Equations

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

def Lean.Parser.Tactic.grind : ParserDescr

Equations

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

def Lean.Parser.Tactic.grindTrace : ParserDescr

Equations

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