inductive Lean.Meta.Grind.SplitStatus : Type

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

instance Lean.Meta.Grind.instInhabitedSplitStatus : Inhabited SplitStatus

Equations

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

instance Lean.Meta.Grind.instBEqSplitStatus : BEq SplitStatus

Equations

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

instance Lean.Meta.Grind.instReprSplitStatus : Repr SplitStatus

Equations

• Lean.Meta.Grind.instReprSplitStatus = { reprPrec := Lean.Meta.Grind.reprSplitStatus✝ }

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) = Lean.Meta.Grind.checkDefaultSplitStatus✝ e
• Lean.Meta.Grind.checkSplitStatus (Lean.Meta.Grind.SplitInfo.imp e h) = Lean.Meta.Grind.checkForallStatus✝ e h
• Lean.Meta.Grind.checkSplitStatus (Lean.Meta.Grind.SplitInfo.arg a b i eq) = Lean.Meta.Grind.checkSplitInfoArgStatus a b eq

def Lean.Meta.Grind.splitNext : GrindTactic

Selects a case-split from the list of candidates, and returns a new list of goals if successful.

Equations

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