def Lean.Meta.Grind.tryFallback : GoalM Bool

Equations

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

def Lean.Meta.Grind.solve (goal : Goal) : GrindM (Option Goal)

Try to solve/close the given goal. Returns some goal if this subgoal failed to be closed, and none if all subgoals were closed.

Equations

• Lean.Meta.Grind.solve goal = do let __discr ← Lean.Meta.Grind.SearchM.run goal Lean.Meta.Grind.solve.main match __discr with | (failed?, snd) => pure failed?

def Lean.Meta.Grind.solve.main : SearchM (Option Goal)

Equations

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

def Lean.Meta.Grind.solve.loop : SearchM (Option Goal)

Equations

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