mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
fe3ba4dc4c
This PR makes the `omit`, `unusedSectionVars` and `loopingSimpArgs` linters respect the `linter.all` option: when `linter.all` is set to false (and the respective linter option is unset), the linter should not report errors. Similarly to #12559, these linters should honour the linter.all flag being set to false. These are all remaining occurrences of this pattern. This fixes an issue analogous to #12559. This PR and #12560 fix all occurrences of this pattern. (The only question is around `RCases.linter.unusedRCasesPattern`: should this also respect this? I have left this alone for now.) Co-authored-by: fiforeach <249703130+fiforeach@users.noreply.github.com>
10 lines
676 B
Plaintext
10 lines
676 B
Plaintext
op_comp: [@Quiver.Hom.op #7 _ #4 #2 (@CategoryStruct.comp _ #6 #4 #3 #2 #1 #0)]
|
|
op_comp: [@CategoryStruct.comp (Opposite #7) _ (@op _ #2) (@op _ #3) (@op _ #4) (@Quiver.Hom.op _ _ #3 #2 #0) (@Quiver.Hom.op _ _ #4 #3 #1)]
|
|
grind_11545.lean:132:4-132:14: warning: declaration uses `sorry`
|
|
grind_11545.lean:148:4-148:13: warning: declaration uses `sorry`
|
|
grind_11545.lean:148:4-148:13: warning: declaration uses `sorry`
|
|
grind_11545.lean:151:4-151:21: warning: declaration uses `sorry`
|
|
grind_11545.lean:154:4-154:21: warning: declaration uses `sorry`
|
|
grind_11545.lean:170:8-170:22: warning: declaration uses `sorry`
|
|
grind_11545.lean:223:8-223:29: warning: declaration uses `sorry`
|