def Lean.Meta.Grind.getDefaultExtensionState : MetaM ExtensionState

Returns the ExtensionState for the default grind attribute.

Equations

• Lean.Meta.Grind.getDefaultExtensionState = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.grindExt __do_lift)

def Lean.Meta.Grind.getOnlyExtensionState : MetaM ExtensionState

Equations

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

def Lean.Meta.Grind.getLiaExtensions : MetaM ExtensionStateArray

Returns the extensions used by the lia tactic.

lia keeps the structural part of the default grind attribute (cases types, funCC, and extensionality theorems), but instead of the full @[grind] E-matching lemma set it only uses the dedicated @[lia] lemma set. This lets cutsat benefit from a small amount of instantiation (e.g. Nat.max_def) without pulling in everything tagged @[grind].

Equations

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

structure Lean.Meta.Grind.Params : Type

• config : Grind.Config
• extensions : ExtensionStateArray
• extra : PArray EMatchTheorem
• extraInj : PArray InjectiveTheorem
• extraFacts : PArray Expr
• symPrios : SymbolPriorities
• norm : Simp.Context
• normProcs : Array Simprocs
• anchorRefs? : Option (Array AnchorRef)

def Lean.Meta.Grind.mkParams (config : Grind.Config) (extensions : ExtensionStateArray) : MetaM Params

Equations

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

def Lean.Meta.Grind.mkDefaultParams (config : Grind.Config) : MetaM Params

Equations

• Lean.Meta.Grind.mkDefaultParams config = do let __do_lift ← Lean.Meta.Grind.getDefaultExtensionState Lean.Meta.Grind.mkParams config #[__do_lift]

def Lean.Meta.Grind.mkOnlyParams (config : Grind.Config) : MetaM Params

Equations

• Lean.Meta.Grind.mkOnlyParams config = do let __do_lift ← Lean.Meta.Grind.getOnlyExtensionState Lean.Meta.Grind.mkParams config #[__do_lift]

def Lean.Meta.Grind.mkMethods (evalTactic? : Option EvalTactic := none) : CoreM Methods

Equations

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

def Lean.Meta.Grind.GrindM.run {α : Type} (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α

Equations

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

def Lean.Meta.Grind.assertExtra (params : Params) : GoalM Unit

Asserts extra facts provided as grind parameters.

Equations

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

def Lean.Meta.Grind.mkGoalCore (mvarId : MVarId) : GrindM Goal

Returns a new goal for the given metavariable.

Equations

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

structure Lean.Meta.Grind.Result : Type

• failure? : Option Goal
• issues : List MessageData
• config : Grind.Config
• counters : Counters
• simp : Simp.Stats
• splitDiags : PArray SplitDiagInfo
• ematchDiags : PArray EMatchDiagInfo

def Lean.Meta.Grind.Result.hasFailed (r : Result) : Bool

Equations

• r.hasFailed = r.failure?.isSome

def Lean.Meta.Grind.Result.toMessageData (result : Result) : MetaM MessageData

Equations

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

def Lean.Meta.Grind.checkUnusedActivations (mvarId : MVarId) (counters : Counters) : GrindM Unit

Checks whether any E-matching lemmas were activated but do not appear in the final proof term. Controlled by set_option grind.unusedLemmaThreshold. Uses grind's instance-marking infrastructure for precise tracking.

Equations

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

def Lean.Meta.Grind.processHypotheses (goal : Goal) (num? : Option Nat := none) : GrindM Goal

When Config.revert := false, we preprocess the hypotheses, and add them to the grind state. It starts at goal.nextDeclIdx. If num? is some num, then at most num local declarations are processed. Otherwise, all remaining local declarations are processed.

Remark: this function assumes the local context does not contains holes with none in decls.

Equations

• Lean.Meta.Grind.processHypotheses goal num? = Lean.Meta.Grind.GoalM.run' goal (discard (Lean.Meta.Grind.processHypotheses.go✝ goal num?).run)

def Lean.Meta.Grind.traceEMatchDiagsCompact (diag : PArray EMatchDiagInfo) : GrindM Unit

Equations

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

def Lean.Meta.Grind.mkResult (params : Params) (failure? : Option Goal) : GrindM Result

Equations

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

def Lean.Meta.Grind.GrindM.runAtGoal {α : Type} (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) (evalTactic? : Option EvalTactic := none) : MetaM α

Equations

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

def Lean.Meta.Grind.main (mvarId : MVarId) (params : Params) : MetaM Result

Equations

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

def Lean.Meta.Grind.withProtectedMCtx {m : Type → Type} {α : Type} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] [MonadExcept Exception m] [MonadRuntimeException m] (config : Grind.Config) (mvarId : MVarId) (k : MVarId → m α) : m α

A helper combinator for executing a grind-based terminal tactic. Given an input goal mvarId, it cleans up local hypotheses corresponding to internal details, creates an auxiliary meta-variable mvarId', and executes k mvarId'. withNewMCtxDepth is used to prevent metavariables from being accidentally assigned by grind's isDefEq calls. After grind finishes, delayed metavariable assignments are resolved, and the resulting proof is assigned to the original goal.

See issue #11806 and issue #12242 for motivating examples.

Equations

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