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

Equations

• Lean.Meta.Grind.mkParams config = do let norm ← Lean.Meta.Grind.getSimpContext config let normProcs ← Lean.Meta.Grind.getSimprocs pure { config := config, norm := norm, normProcs := normProcs }

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

Equations

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

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

Equations

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

structure Lean.Meta.Grind.Result : Type

• failures : List Goal
• skipped : List Goal
• issues : List MessageData
• config : Grind.Config
• trace : Trace
• counters : Counters
• simp : Simp.Stats

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

Equations

• r.hasFailures = !r.failures.isEmpty

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.main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result

Equations

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