def Lean.Meta.Grind.checkSolvers : SearchM Bool

Equations

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

def Lean.Meta.Grind.ematchStep : SearchM Bool

Equations

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

def Lean.Meta.Grind.mbtcStep : SearchM Bool

Equations

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

def Lean.Meta.Grind.lookaheadStep : SearchM 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?