chore(*): remove comments mentioning obsolete note [nolint_ge]#37503
chore(*): remove comments mentioning obsolete note [nolint_ge]#37503Vierkantor wants to merge 1 commit intoleanprover-community:masterfrom
[nolint_ge]#37503Conversation
In Lean 3 times we used to have a `ge_or_gt` linter which complained if theorem statements contained `≥` or `>`, and it would be silenced with a reference to the library note `[nolint_ge]`. But the linter and its note never got ported, so the references are irrelevant and we should drop them.
Vierkantor
added
t-linter
PR summary 551ca8f603Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
I have an (old) PR porting the linter: #12879 --- that got stalled because there was no decision if we still want the linter. My understanding is that
|
|
If there is agreement that the linter is desirable, I'm happy to dust off my PR. I don't have spoons this week to start a discussion about this, though. |
|
I don't recall seeing issues with tactics failing to unify |
2 participants
In Lean 3 times we used to have a
ge_or_gtlinter which complained if theorem statements contained≥or>, and it would be silenced with a reference to the library note[nolint_ge]. But the linter and its note never got ported, so the references are irrelevant and we should drop them.