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

Equations

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

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

Equations

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

def Lean.Meta.Grind.all (goals : List Lean.Meta.Grind.Goal) (f : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal)) : Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal)

Equations

• Lean.Meta.Grind.all goals f = List.foldlM (fun (acc : List Lean.Meta.Grind.Goal) (goal : Lean.Meta.Grind.Goal) => do let __do_lift ← f goal pure (acc ++ __do_lift)) [] goals

def Lean.Meta.Grind.main (mvarId : Lean.MVarId) (config : Lean.Grind.Config) (mainDeclName : Lean.Name) (fallback : Lean.Meta.Grind.Fallback) : Lean.MetaM (List Lean.MVarId)

Equations

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