-
Notifications
You must be signed in to change notification settings - Fork 316
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] - chore(Algebra/Ring): remove variables unused in section #17178
Conversation
PR summary 8f2d3164d5Import 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/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> The doc-module for |
This seems like a fun linter to write! Environment linters don't know about I'll try to see if something can be done! |
Bhavik, I wrote a linter and these are the first unused variables found: #17261. There are many more: some are potential false positives, since the linter is not really able to deal with declarations that use the equation compiler, but a lot of the output are actually unused variables. |
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by adomani. |
Inspired by #17178 and found by a linter.
bors merge |
Perhaps we should have a linter for this... @adomani?
Pull request successfully merged into master. Build succeeded: |
Inspired by #17178 and found by a linter.
Perhaps we should have a linter for this... @adomani?
Inspired by #17178 and found by a linter.
Perhaps we should have a linter for this... @adomani?
Perhaps we should have a linter for this... @adomani?