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) (config : Grind.Config) (fallback : Fallback) : MetaM α

Equations

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

def Lean.Meta.Grind.all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List 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 : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId)

Equations

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