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 acasesOn
application containing meta-variables. Subgoals that still need to be processed.
- generation : Nat
Instances For
Equations
Instances For
Equations
- Lean.Meta.Grind.getGoal = do let __do_lift ← get pure __do_lift.goal
Instances For
Equations
- Lean.Meta.Grind.setGoal goal = modify fun (s : Lean.Meta.Grind.SearchM.State) => { goal := goal, choiceStack := s.choiceStack }
Instances For
Equations
- Lean.Meta.Grind.withCurrGoalContext x = do let __do_lift ← Lean.Meta.Grind.getGoal __do_lift.mvarId.withContext x
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Grind.instMonadLiftGoalMSearchM = { monadLift := fun {α : Type} => Lean.Meta.Grind.liftGoalM }
Equations
- Lean.Meta.Grind.SearchM.run goal x = goal.mvarId.withContext (StateRefT'.run x { goal := goal })
Instances For
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 usingproof
, and update current goal usings
. - 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 withs
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.