[Merged by Bors] - chore: remove some unused variables#31017
[Merged by Bors] - chore: remove some unused variables#31017Ruben-VandeVelde wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
Ruben-VandeVelde
commented
Oct 28, 2025
PR summary 31f931fed0Import 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 No changes to technical debt.You can run this locally as
|
| section Mul | ||
|
|
||
| variable [Mul M] [One M] {l : List M} {a : M} | ||
| variable [Mul M] [One M] {a : M} {l : List M} |
There was a problem hiding this comment.
Why swap these? I usually like to put the most bundled ones first
There was a problem hiding this comment.
Just to not change the signature of prod_cons (which is the only one that uses a in this section); I'd rather avoid any visible changes in this PR, even if it's quite unlikely that it'd affect anything in this case.
There was a problem hiding this comment.
Sure, but you are changing the signature of other lemmas instead, so I don't really see the point
There was a problem hiding this comment.
Oh I guess there are no other lemmas in this instance. Still, I wouldn't bother
|
Thanks! maintainer delegate |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Pull request successfully merged into master. Build succeeded: |