inductive Lean.Meta.Grind.CaseSplitStatus : Type

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

Instances For

• Lean.Meta.Grind.instBEqCaseSplitStatus
• Lean.Meta.Grind.instInhabitedCaseSplitStatus

instance Lean.Meta.Grind.instInhabitedCaseSplitStatus : Inhabited CaseSplitStatus

Equations

• Lean.Meta.Grind.instInhabitedCaseSplitStatus = { default := Lean.Meta.Grind.CaseSplitStatus.resolved }

instance Lean.Meta.Grind.instBEqCaseSplitStatus : BEq CaseSplitStatus

Equations

• Lean.Meta.Grind.instBEqCaseSplitStatus = { beq := Lean.Meta.Grind.beqCaseSplitStatus✝ }

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.