Documentation

Lean.Meta.Match.CaseArraySizes

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

Split goal ... |- C a into sizes.size + 1 subgoals

  1. ..., x_1 ... x_{sizes[0]} |- C #[x_1, ... x_{sizes[0]}] ... n) ..., x_1 ... x_{sizes[n-1]} |- C #[x_1, ..., x_{sizes[n-1]}] n+1) ..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a where n = sizes.size
Equations
  • One or more equations did not get rendered due to their size.