structure Lean.Meta.CaseValueSubgoal : Type

• mvarId : Lean.MVarId
• newH : Lean.FVarId
• subst : Lean.Meta.FVarSubst

instance Lean.Meta.instInhabitedCaseValueSubgoal : Inhabited Lean.Meta.CaseValueSubgoal

Equations

• Lean.Meta.instInhabitedCaseValueSubgoal = { default := { mvarId := default, newH := default, subst := default } }

def Lean.Meta.caseValue (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (value : Lean.Expr) : Lean.MetaM (Lean.Meta.CaseValueSubgoal × Lean.Meta.CaseValueSubgoal)

Equations

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

structure Lean.Meta.CaseValuesSubgoal : Type

• mvarId : Lean.MVarId
• newHs : Array Lean.FVarId
• subst : Lean.Meta.FVarSubst

instance Lean.Meta.instInhabitedCaseValuesSubgoal : Inhabited Lean.Meta.CaseValuesSubgoal

def Lean.Meta.caseValues (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (values : Array Lean.Expr) (hNamePrefix : Lean.Name := `h) (substNewEqs : Bool := false) : Lean.MetaM (Array Lean.Meta.CaseValuesSubgoal)

Split goal ... |- C x into values.size + 1 subgoals

1. ..., (h_1 : x = value[0]) |- C value[0] ... n) ..., (h_n : x = value[n - 1]) |- C value[n - 1] n+1) ..., (h_1 : x != value[0]) ... (h_n : x != value[n-1]) |- C x where n = values.size where fvarId is xs id. The type of x must have decidable equality.

Remark: the last subgoal is for the "else" catchall case, and its subst is {}. Remark: the field newHs has size 1 forall but the last subgoal.

If substNewEqs = true, then the new h_i equality hypotheses are substituted in the first n cases.

def Lean.Meta.caseValues.loop (fvarId : Lean.FVarId) (hNamePrefix : Lean.Name := `h) (substNewEqs : Bool := false) : Nat → Lean.MVarId → List Lean.Expr → Array Lean.FVarId → Array Lean.Meta.CaseValuesSubgoal → Lean.MetaM (Array Lean.Meta.CaseValuesSubgoal)