inductive Lean.Meta.Grind.ProofStep : Type

Helper type for implementing finish? and grind?

• solver (id : Nat) : ProofStep
• lookahead : ProofStep
• mbtc : ProofStep
• instantiate (thms usedThms : List EMatchTheorem) : ProofStep

def Lean.Meta.Grind.instInhabitedProofStep.default : ProofStep

Equations

• Lean.Meta.Grind.instInhabitedProofStep.default = Lean.Meta.Grind.ProofStep.solver default

instance Lean.Meta.Grind.instInhabitedProofStep : Inhabited ProofStep

Equations

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

inductive Lean.Meta.Grind.ProofTrace : Type

Helper type for implementing finish? and grind?

• done : ProofTrace
• sep (s : ProofStep) (k : ProofTrace) : ProofTrace
• cases (info : SplitInfo) (alts : List ProofTrace) : ProofTrace

def Lean.Meta.Grind.instInhabitedProofTrace.default : ProofTrace

Equations

• Lean.Meta.Grind.instInhabitedProofTrace.default = Lean.Meta.Grind.ProofTrace.done

instance Lean.Meta.Grind.instInhabitedProofTrace : Inhabited ProofTrace

Equations

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

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.

• traces : Array ProofTrace
• generation : Nat

instance Lean.Meta.Grind.instInhabitedChoice : Inhabited Choice

Equations

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

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

Equations

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

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

• goal : Goal
• steps : Array ProofStep
• trace? : Option ProofTrace
• 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, steps := s.steps, trace? := s.trace?, 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.