def Lean.Meta.Grind.getDefaultExtensionState : MetaM ExtensionState

Returns the ExtensionState for the default grind attribute.

def Lean.Meta.Grind.getOnlyExtensionState : MetaM ExtensionState

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

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

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

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

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

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

Asserts extra facts provided as grind parameters.

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

Returns a new goal for the given metavariable.

structure Lean.Meta.Grind.Result : Type

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

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

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

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.

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

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

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

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.