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

instance Lean.Meta.Grind.instInhabitedSplitStatus : Inhabited SplitStatus

instance Lean.Meta.Grind.instBEqSplitStatus : BEq SplitStatus

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

instance Lean.Meta.Grind.instReprSplitStatus : Repr SplitStatus

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

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

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

structure Lean.Meta.Grind.SplitCandidateWithAnchor : Type

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

instance Lean.Meta.Grind.instHasAnchorSplitCandidateWithAnchor : HasAnchor SplitCandidateWithAnchor

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.

def Lean.Meta.Grind.Action.isSorryAlt (alt : List (TSyntax `grind)) : Bool

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.

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