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.instInhabitedSplitStatus.default }

def Lean.Meta.Grind.instInhabitedSplitStatus.default : 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.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

instance Lean.Meta.Grind.instReprSplitStatus : Repr SplitStatus

Equations

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

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

Equations

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

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

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.

Equations

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