New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(lint): improved ge_or_gt linter #3810
Conversation
016fa09
to
10f925f
Compare
10f925f
to
2e135a1
Compare
@@ -1262,7 +1262,7 @@ lemma remove_nth_insert_nth (n:ℕ) (l : list α) : (l.insert_nth n a).remove_nt | |||
by rw [remove_nth_eq_nth_tail, insert_nth, modify_nth_tail_modify_nth_tail_same]; | |||
from modify_nth_tail_id _ _ | |||
|
|||
lemma insert_nth_remove_nth_of_ge : ∀n m as, n < length as → m ≥ n → | |||
lemma insert_nth_remove_nth_of_ge : ∀n m as, n < length as → n ≤ m → |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should the name be changed too?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maybe... However, insert_nth_remove_nth_of_le
already exists, with n
and m
in the other order.
bors merge |
The linter will now correctly accepts occurrences of `f (≥)` and `∃ x ≥ t, b` The linter will still raise a false positive on `∃ x y ≥ t, b` (with 2+ bound variables in a single binder that involves `>/≥`) In contrast to the previous version of the linter, this one *does* check hypotheses. This should reduce the `@[nolint ge_or_gt]` attributes from ~160 to ~10.
Pull request successfully merged into master. Build succeeded: |
The linter will now correctly accepts occurrences of
f (≥)
and∃ x ≥ t, b
The linter will still raise a false positive on
∃ x y ≥ t, b
(with 2+ bound variables in a single binder that involves>/≥
)In contrast to the previous version of the linter, this one does check hypotheses.
This should reduce the
@[nolint ge_or_gt]
attributes from ~160 to ~10.Until #3808 and #3809 are merged, the linter will raise many errors.