structure Lean.Meta.Grind.Params : Type

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

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

def Lean.Meta.Grind.mkMethods (fallback : Fallback) : CoreM Methods

def Lean.Meta.Grind.GrindM.run {α : Type} (x : GrindM α) (params : Params) (fallback : Fallback) : MetaM α

structure Lean.Meta.Grind.Result : Type

• failure? : Option Goal
• issues : List MessageData
• config : Grind.Config
• trace : Trace
• counters : Counters
• simp : Simp.Stats

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

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

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