structure Lean.Meta.Grind.Params : Type

• config : Grind.Config
• ematch : EMatchTheorems
• inj : InjectiveTheorems
• symPrios : SymbolPriorities
• casesTypes : CasesTypes
• extra : PArray EMatchTheorem
• norm : Simp.Context
• normProcs : Array Simprocs

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
• trace : Trace
• 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.