inductive Lean.Meta.Grind.SplitStatus : Type

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

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedSplitStatus : Inhabited SplitStatus

@[instance_reducible]

instance Lean.Meta.Grind.instBEqSplitStatus : BEq SplitStatus

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

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

@[instance_reducible]

instance Lean.Meta.Grind.instReprSplitStatus : Repr SplitStatus

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_reducible]

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) (candidates? : Option (List SplitInfo) := none) : GoalM SplitCandidateAnchors

Returns case-split candidates. Case-splits that are tagged as .resolved or .notReady are skipped. Applies additional filter if provided. If candidates? is provided, it is used instead of the candidates stored in the goal.

structure Lean.Meta.Grind.SplitAnchorRefInfo : Type

Anchor reference for a case-split candidate in generated tactic scripts. ordinal is the 0-based position of the candidate among the (ready) candidates whose anchors share the same displayed prefix. Distinct candidates may have identical anchors (e.g., candidates that differ only in inaccessible variables), and the ordinal is used to disambiguate them.

• numDigits : Nat
• anchor : UInt64
• ordinal : Nat

def Lean.Meta.Grind.mkSplitAnchorRefInfo (c : SplitInfo) (candidates? : Option (List SplitInfo) := none) : GoalM SplitAnchorRefInfo

Computes the anchor reference information for the case-split candidate c. The candidate list must be the one stored in the goal before the case-split is selected and performed (i.e., before selectNextSplit? prunes the list and before c is marked as resolved), so that it matches the list inspected by the cases tactic when replaying the generated script.

def Lean.Meta.Grind.SplitAnchorRefInfo.toSyntax (info : SplitAnchorRefInfo) : CoreM (TSyntax `grind)

Creates the anchor reference syntax for the result of mkSplitAnchorRefInfo.

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) (candidates? : Option (List SplitInfo) := none) : 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