structure Lean.Meta.CaseValuesSubgoal : Type

• mvarId : MVarId
• newHs : Array FVarId
• subst : FVarSubst

def Lean.Meta.instInhabitedCaseValuesSubgoal.default : CaseValuesSubgoal

Equations

• Lean.Meta.instInhabitedCaseValuesSubgoal.default = { mvarId := default, newHs := default, subst := default }

instance Lean.Meta.instInhabitedCaseValuesSubgoal : Inhabited CaseValuesSubgoal

Equations

• Lean.Meta.instInhabitedCaseValuesSubgoal = { default := Lean.Meta.instInhabitedCaseValuesSubgoal.default }

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

Split goal ... |- C x, where fvarId is xs id, 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 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 needsHyps = false then the else case comes without hypotheses.

Equations

• Lean.Meta.caseValues mvarId fvarId values hNamePrefix needHyps = Lean.Meta.caseValues.loop✝ fvarId hNamePrefix needHyps 1 mvarId values.toList #[] #[]