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

Instances For

• Lean.Meta.Grind.instInhabitedChoice

instance Lean.Meta.Grind.instInhabitedChoice : Inhabited Choice

Equations

• Lean.Meta.Grind.instInhabitedChoice = { default := { goalPending := default, proof := default, todo := default, generation := 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

Instances For

• Lean.Meta.Grind.instMonadLiftGoalMSearchM

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) : 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.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.

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.