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

instance Lean.Meta.Grind.instBEqSplitStatus : BEq SplitStatus

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

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.