inductive Lean.Meta.Grind.SplitStatus : Type

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

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSplitStatus : Inhabited SplitStatus

Equations

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

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqSplitStatus : BEq SplitStatus

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Lean.Meta.Grind.instReprSplitStatus : Repr SplitStatus

Equations

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

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

@[implicit_reducible]

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) (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.

Equations

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

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.

Equations

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

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

Creates the anchor reference syntax for the result of mkSplitAnchorRefInfo.

Equations

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

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

Equations

• Lean.Meta.Grind.Action.isSorryAlt [tac] = if tac.raw.isOfKind `Lean.Parser.Tactic.Grind.sorry = true then have __discr := tac.raw.getArg 0; true else have __discr := tac; false
• Lean.Meta.Grind.Action.isSorryAlt alt = false

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.

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.