Documentation

Lean.Meta.Match.CaseValues

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

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 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