-
Notifications
You must be signed in to change notification settings - Fork 299
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] - fix(tactic/lint/basic): remove default argument for auto_decl and enable more linters #2580
Conversation
@@ -55,10 +55,10 @@ begin | |||
{ assume h, subst h, exact forall₂_refl _ } | |||
end | |||
|
|||
@[simp] lemma forall₂_nil_left_iff {l} : forall₂ r nil l ↔ l = nil := | |||
@[simp, priority 900] lemma forall₂_nil_left_iff {l} : forall₂ r nil l ↔ l = nil := |
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.
Why is this in this PR?
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.
Because they overlap with another simp lemma:
mathlib/src/data/list/defs.lean
Line 279 in 67f3fde
attribute [simp] forall₂.nil |
The forall₂.nil
lemma is a constructor, and therefore the linter did not catch this issue before.
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.
OK, thanks.
bors r+ |
…ble more linters (#2580) Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the `auto_decls` flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856
Pull request successfully merged into master. Build succeeded: |
…ble more linters (#2580) Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the `auto_decls` flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856
…ble more linters (leanprover-community#2580) Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the `auto_decls` flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856
…ble more linters (leanprover-community#2580) Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the `auto_decls` flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856
…ble more linters (leanprover-community#2580) Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the `auto_decls` flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856
Run more linters on automatically-generated declarations. Quite a few linters should have been run on them, but I forgot about it because the
auto_decls
flag is optional and off by default. I've made it non-optional so that you don't forget about it when defining a linter.https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20linter.20and.20structure.20fields/near/195810856