structure Lean.Meta.CaseValueSubgoal : Type

• mvarId : MVarId
• newH : FVarId
• subst : FVarSubst

instance Lean.Meta.instInhabitedCaseValueSubgoal : Inhabited CaseValueSubgoal

Equations

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

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

Equations

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

structure Lean.Meta.CaseValuesSubgoal : Type

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

instance Lean.Meta.instInhabitedCaseValuesSubgoal : Inhabited CaseValuesSubgoal

Equations

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

def Lean.Meta.caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNamePrefix : Name := `h) (substNewEqs : Bool := false) : MetaM (Array 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.

Equations

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

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