structure Lean.Meta.Grind.Solve.State : Type

• todo : List Goal
• failures : List Goal
• stop : Bool

def Lean.Meta.Grind.Solve.getNext? : Lean.Meta.Grind.Solve.M✝ (Option Goal)

Equations

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

def Lean.Meta.Grind.Solve.pushGoal (goal : Goal) : Lean.Meta.Grind.Solve.M✝ Unit

Equations

• Lean.Meta.Grind.Solve.pushGoal goal = modify fun (s : Lean.Meta.Grind.Solve.State) => { todo := goal :: s.todo, failures := s.failures, stop := s.stop }

def Lean.Meta.Grind.Solve.pushGoals (goals : List Goal) : Lean.Meta.Grind.Solve.M✝ Unit

Equations

• Lean.Meta.Grind.Solve.pushGoals goals = modify fun (s : Lean.Meta.Grind.Solve.State) => { todo := goals ++ s.todo, failures := s.failures, stop := s.stop }

def Lean.Meta.Grind.Solve.pushFailure (goal : Goal) : Lean.Meta.Grind.Solve.M✝ Unit

Equations

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

@[inline]

def Lean.Meta.Grind.Solve.stepGuard (x : Goal → Lean.Meta.Grind.Solve.M✝ Bool) (goal : Goal) : Lean.Meta.Grind.Solve.M✝ Bool

Equations

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

def Lean.Meta.Grind.Solve.applyTac (x : GrindTactic) (goal : Goal) : Lean.Meta.Grind.Solve.M✝ Bool

Equations

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

def Lean.Meta.Grind.Solve.tryAssertNext : Goal → Lean.Meta.Grind.Solve.M✝ Bool

Equations

• Lean.Meta.Grind.Solve.tryAssertNext = Lean.Meta.Grind.Solve.applyTac Lean.Meta.Grind.assertNext

def Lean.Meta.Grind.Solve.tryEmatch : Goal → Lean.Meta.Grind.Solve.M✝ Bool

Equations

• Lean.Meta.Grind.Solve.tryEmatch = Lean.Meta.Grind.Solve.applyTac Lean.Meta.Grind.ematchAndAssert

def Lean.Meta.Grind.Solve.trySplit : Goal → Lean.Meta.Grind.Solve.M✝ Bool

Equations

• Lean.Meta.Grind.Solve.trySplit = Lean.Meta.Grind.Solve.applyTac Lean.Meta.Grind.splitNext

def Lean.Meta.Grind.Solve.maxNumFailuresReached : Lean.Meta.Grind.Solve.M✝ Bool

Equations

• Lean.Meta.Grind.Solve.maxNumFailuresReached = do let __do_lift ← get let __do_lift_1 ← liftM Lean.Meta.Grind.getConfig pure (decide (__do_lift.failures.length ≥ __do_lift_1.failures))

def Lean.Meta.Grind.Solve.main (fallback : Fallback) : Lean.Meta.Grind.Solve.M✝ Unit

Equations

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

def Lean.Meta.Grind.solve (goals : List Goal) (fallback : Fallback) : GrindM (List Goal × List Goal)

Try to solve/close the given goals, and returns the ones that could not be solved.

Equations

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