inductive Lean.Meta.Grind.SplitStatus : Type

• resolved : SplitStatus
• notReady : SplitStatus
• ready (numCases : Nat) (isRec tryPostpone : Bool := false) : SplitStatus

def Lean.Meta.Grind.instInhabitedSplitStatus.default : SplitStatus

Equations

• Lean.Meta.Grind.instInhabitedSplitStatus.default = Lean.Meta.Grind.SplitStatus.resolved

instance Lean.Meta.Grind.instInhabitedSplitStatus : Inhabited SplitStatus

Equations

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

def Lean.Meta.Grind.instBEqSplitStatus.beq : SplitStatus → SplitStatus → Bool

Equations

• Lean.Meta.Grind.instBEqSplitStatus.beq Lean.Meta.Grind.SplitStatus.resolved Lean.Meta.Grind.SplitStatus.resolved = true
• Lean.Meta.Grind.instBEqSplitStatus.beq Lean.Meta.Grind.SplitStatus.notReady Lean.Meta.Grind.SplitStatus.notReady = true
• Lean.Meta.Grind.instBEqSplitStatus.beq (Lean.Meta.Grind.SplitStatus.ready a a_1 a_2) (Lean.Meta.Grind.SplitStatus.ready b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.Grind.instBEqSplitStatus.beq x✝¹ x✝ = false

instance Lean.Meta.Grind.instBEqSplitStatus : BEq SplitStatus

Equations

• Lean.Meta.Grind.instBEqSplitStatus = { beq := Lean.Meta.Grind.instBEqSplitStatus.beq }

instance Lean.Meta.Grind.instReprSplitStatus : Repr SplitStatus

Equations

• Lean.Meta.Grind.instReprSplitStatus = { reprPrec := Lean.Meta.Grind.instReprSplitStatus.repr }

def Lean.Meta.Grind.instReprSplitStatus.repr : SplitStatus → Nat → Format

Equations

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

def Lean.Meta.Grind.checkSplitInfoArgStatus (a b eq : Expr) : GoalM SplitStatus

Equations

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

def Lean.Meta.Grind.checkSplitStatus (s : SplitInfo) : GoalM SplitStatus

Equations

• Lean.Meta.Grind.checkSplitStatus (Lean.Meta.Grind.SplitInfo.default e source) = Lean.Meta.Grind.checkDefaultSplitStatus✝ e
• Lean.Meta.Grind.checkSplitStatus (Lean.Meta.Grind.SplitInfo.imp e h source) = Lean.Meta.Grind.checkForallStatus✝ e h
• Lean.Meta.Grind.checkSplitStatus (Lean.Meta.Grind.SplitInfo.arg a b i eq source) = Lean.Meta.Grind.checkSplitInfoArgStatus a b eq

structure Lean.Meta.Grind.SplitCandidateWithAnchor : Type

• c : SplitInfo
• numCases : Nat
• isRec : Bool
• e : Expr
• anchor : UInt64

instance Lean.Meta.Grind.instHasAnchorSplitCandidateWithAnchor : HasAnchor SplitCandidateWithAnchor

Equations

• Lean.Meta.Grind.instHasAnchorSplitCandidateWithAnchor = { getAnchor := fun (e : Lean.Meta.Grind.SplitCandidateWithAnchor) => e.anchor }

structure Lean.Meta.Grind.SplitCandidateAnchors : Type

• candidates : Array SplitCandidateWithAnchor

  Pairs (anchor, split)

• numDigits : Nat

  Number of digits (≥ 4) sufficient for distinguishing anchors. We usually display only the first numDigits.

def Lean.Meta.Grind.getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun (x : Expr) => pure true) : GoalM SplitCandidateAnchors

Returns case-split candidates. Case-splits that are tagged as .resolved or .notReady are skipped. Applies additional filter if provided.

Equations

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

def Lean.Meta.Grind.Action.splitCore (c : SplitInfo) (numCases : Nat) (isRec stopAtFirstFailure compress : Bool) : Action

Performs a case-split using c. Remark: numCases and isRec are computed using checkSplitStatus.

Equations

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

def Lean.Meta.Grind.Action.splitNext (stopAtFirstFailure compress : Bool := true) : Action

Selects a case-split from the list of candidates, performs the split and applies continuation to all subgoals. If a subgoal is solved without using new hypotheses, closes the original goal using this proof. That is, it performs non-chronological backtracking.

If stopsAtFirstFailure = true, it stops the search as soon as the given continuation cannot solve a subgoal.

If compress = true, then it uses <;> to generate the resulting tactic sequence if all subgoal sequences are identical. For example, suppose that the following sequence is generated with compress = false

cases #50fc
next => lia
next => lia

Then with compress = true it generates cases #50fc <;> lia

Equations

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

------------------------------------------ ------------------------------------------ TODO Delete rest of the file ------------------------------------------ ------------------------------------------

def Lean.Meta.Grind.splitNext : SearchM Bool

Selects a case-split from the list of candidates, and adds new choice point (aka backtracking point). Returns true if successful.

Equations

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

def Lean.Meta.Grind.split? (c : SplitInfo) : SearchM (Option (List Goal × Nat))

Tries to perform a case-split using c. Returns none if c has already been resolved or is not ready.

Equations

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