structure Lean.Meta.Grind.Choice : Type

A choice (aka backtracking) point in the search tree.

• goalPending : Goal

  Goal where the case-split was performed. Invariant: goalOld.mvarId is not assigned.

• proof : Expr

  Expression to be assigned to goalOld.mvarId if it is not possible to perform non-chronological backtracking. proof is often a casesOn application containing meta-variables.

• todo : List Goal

  Subgoals that still need to be processed.

• generation : Nat

instance Lean.Meta.Grind.instInhabitedChoice : Inhabited Choice

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

• goal : Goal
• choiceStack : List Choice

@[reducible, inline]

abbrev Lean.Meta.Grind.SearchM (α : Type) : Type

def Lean.Meta.Grind.getGoal : SearchM Goal

def Lean.Meta.Grind.setGoal (goal : Goal) : SearchM Unit

@[reducible, inline]

abbrev Lean.Meta.Grind.withCurrGoalContext {α : Type} (x : SearchM α) : SearchM α

@[reducible, inline]

abbrev Lean.Meta.Grind.liftGoalM {α : Type} (x : GoalM α) : SearchM α

instance Lean.Meta.Grind.instMonadLiftGoalMSearchM : MonadLift GoalM SearchM

@[inline]

def Lean.Meta.Grind.SearchM.run {α : Type} (goal : Goal) (x : SearchM α) : GrindM (α × State)

def Lean.Meta.Grind.mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) : SearchM Unit

Given a proof containing meta-variables corresponding to the given subgoals, create a choice point.

• If there are no choice points, we just close the current goal using proof.
• If there is only one subgoal s, we close the current goal using proof, and update current goal using s.
• If there are more than one s :: ss, we create a choice point using the current goal as the pending goal, and update the current goal with s.

def Lean.Meta.Grind.mkAuxMVarForCurrGoal : SearchM MVarId

Create an auxiliary metavariable with the same type and tag of the metavariable associated with the current goal. We use this function to perform cases on the current goal without eagerly assignining it.

def Lean.Meta.Grind.nextGoal? : SearchM (Option Nat)

Select the next goal to be processed from the choiceStack. This function assumes the current goal has been closed (i.e., inconsistent is true) Returns some gen if a new goal was found for a choice point with generation gen, and returns none otherwise.