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 first abstracts meta-variables, cleans up local hypotheses corresponding to internal details, creates an auxiliary meta-variable mvarId', and executes k mvarId'. The execution is performed in a new meta-variable context depth to ensure that universe meta-variables cannot be accidentally assigned by grind. If k fails, it admits the input goal.

See issue #11806 for a motivating example.