- mvarId : Lean.MVarId
- newH : Lean.FVarId
- subst : Lean.Meta.FVarSubst
Equations
- Lean.Meta.instInhabitedCaseValueSubgoal = { default := { mvarId := default, newH := default, subst := default } }
Equations
- One or more equations did not get rendered due to their size.
- mvarId : Lean.MVarId
- newHs : Array Lean.FVarId
- subst : Lean.Meta.FVarSubst
Equations
- Lean.Meta.instInhabitedCaseValuesSubgoal = { default := { mvarId := default, newHs := default, subst := default } }
def
Lean.Meta.caseValues
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
(values : Array Lean.Expr)
(hNamePrefix : optParam Lean.Name `h)
(substNewEqs : optParam Bool false)
:
Split goal ... |- C x into values.size + 1 subgoals
..., (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 xwheren = values.sizewherefvarIdisxs id. The type ofxmust have decidable equality.
Remark: the last subgoal is for the "else" catchall case, and its subst is {}.
Remark: the fiels 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 (Array.toList values) #[] #[]
def
Lean.Meta.caseValues.loop
(fvarId : Lean.FVarId)
(hNamePrefix : optParam Lean.Name `h)
(substNewEqs : optParam Bool false)
: