Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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: have/let linter #12190
[Merged by Bors] - feat: have/let linter #12190
Changes from 2 commits
aaa9d84
30280a5
e25f2e2
09cd667
5bbe4aa
98dbefc
7a4e089
8dbc7fd
0f74c28
27bc724
8a9dbec
159c6e3
c7566c4
3345288
d7241ab
160e2b8
10937ef
9724831
06a9d69
4bd7535
a085a6b
c23b907
4c359f2
d99a922
94894a9
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
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.
Is there a way to guard an unfinished proof, like this one without
tauto
? If I understand your motivation for level1
correctly, it's also to trigger on unfinished proofs, isn't it?I expected that if I delete the
#guard_msgs
here and then deletetauto
that the linter warnings would pop up. Did I understand this wrongly?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.
The linter emits a warning if a declaration simultaneously does not have errors and yet emits messages. Simply removing
tauto
leaves anunsolved goals
error, so the linter shuts up. If, instead, you replacetauto
withsorry
, then the linter will tell you that you should uselet
/have
.I could make the linter chatty also in the presence of errors, but I think that on an erroring declaration, the linter will yield dubious reports and would be simply extra noise.
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. I somehow expect that an "unsolved goals" error behaves very similar to a "declaration uses sorry" warning in as many aspects as possible but I see that's not as easy with how messages are reported.
Looks good to me as is.