source
def Lean.Meta.Grind.checkSolvers :
SearchM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.ematchStep :
SearchM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.mbtcStep :
SearchM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.lookaheadStep :
SearchM Bool
Equations

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

Instances For

source
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?

Instances For