18459cb537
which also removes an error condition at the use site. While I am at it, I rename a parameter in `GuessLex` that I forgot to rename earlier. The effect will be user-visible (in obscure corner cases) with #2960, so I’ll have the test there. A few places would benefit from a `lambdaTelescopeBounded` that garantees the result has the right length (eta-expanding when necessary). I’ll look into that separately, and left TODOs here. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| CaseArraySizes.lean | ||
| CaseValues.lean | ||
| Match.lean | ||
| MatchEqs.lean | ||
| MatchEqsExt.lean | ||
| MatcherInfo.lean | ||
| MatchPatternAttr.lean | ||
| MVarRenaming.lean | ||
| Value.lean | ||