structure Lean.Meta.Grind.Params : Type

• config : Grind.Config
• ematch : EMatchTheorems
• inj : InjectiveTheorems
• symPrios : SymbolPriorities
• casesTypes : CasesTypes
• extra : PArray EMatchTheorem
• extraInj : PArray InjectiveTheorem
• norm : Simp.Context
• normProcs : Array Simprocs
• anchorRefs? : Option (Array AnchorRef)

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

Equations

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

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.

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

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

• Lean.Meta.Grind.GrindM.runAtGoal mvarId params k evalTactic? = (Lean.Meta.withReducible do let goal ← Lean.Meta.Grind.initCore✝ mvarId params k goal).run params evalTactic?

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] (abstractProof : Bool) (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.

Equations

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