lean4-htt/tests/elab/calc.lean.out.expected at master - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Michael Rothgang fe3ba4dc4c

fix: make the omit, unusedSectionVars and loopingSimpArgs linter respect linter.all (#12563 )

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>

2026-03-09 11:58:02 +00:00

1 line

55 B

Text

Raw Permalink Blame History

calc.lean:15:0-15:8: warning: declaration uses `sorry`