structure Lean.Meta.Grind.Choice : Type

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

• info? : Option SplitInfo
• goalPending : Goal

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

• proof : Expr

  Expression to be assigned to goalPending.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

def Lean.Meta.Grind.instInhabitedChoice.default : Choice

Equations

• Lean.Meta.Grind.instInhabitedChoice.default = { info? := default, goalPending := default, proof := default, todo := default, generation := default }

instance Lean.Meta.Grind.instInhabitedChoice : Inhabited Choice

Equations

• Lean.Meta.Grind.instInhabitedChoice = { default := Lean.Meta.Grind.instInhabitedChoice.default }

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

• goal : Goal
• choiceStack : List Choice

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.SearchM = StateRefT' IO.RealWorld Lean.Meta.Grind.SearchM.State Lean.Meta.Grind.GrindM

def Lean.Meta.Grind.getGoal : SearchM Goal

Equations

• Lean.Meta.Grind.getGoal = do let __do_lift ← get pure __do_lift.goal

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

Equations

• Lean.Meta.Grind.setGoal goal = modify fun (s : Lean.Meta.Grind.SearchM.State) => { goal := goal, choiceStack := s.choiceStack }

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.withCurrGoalContext x = do let __do_lift ← Lean.Meta.Grind.getGoal __do_lift.mvarId.withContext x

@[reducible, inline]

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

Equations

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

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

Equations

• Lean.Meta.Grind.instMonadLiftGoalMSearchM = { monadLift := fun {α : Type} => Lean.Meta.Grind.liftGoalM }

@[inline]

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

Equations

• Lean.Meta.Grind.SearchM.run goal x = goal.mvarId.withContext (StateRefT'.run x { goal := goal })

def Lean.Meta.Grind.mkChoice (proof : Expr) (subgoals : List Goal) (generation : Nat) (info? : Option SplitInfo := none) : 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.

Equations

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

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.

Equations

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