[Merged by Bors] - chore: avoid some unused variables #11594
Conversation
Ruben-VandeVelde
added
awaiting-review
| simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one, | ||
| Units.val_one, h] | ||
| · exact h | ||
| refine hzero.resolve_left fun h => ha ?_ |
There was a problem hiding this comment.
Use "\maps" instead of "=>" while you're at it?
There was a problem hiding this comment.
(Not official or anything, but my preference is against "while you're at it" suggestions. They really do, in my opinion, add friction to getting stuff done.)
There was a problem hiding this comment.
I understand this point!
My point was this is a new proof written - so reviewing doesn't become any harder this way. Authoring it does; thanks for pointing this out.
There was a problem hiding this comment.
Let me add: I can make sure to, in the future,
- make such comments directly as suggestions (minimizing the overhead for authors and reviewers)
- limit these comments to new proofs, or PRs cleaning up miscellaneous things, where such a change is in scope.
|
✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors merge |
These will be caught by the linter in a future lean version.
|
Build failed: |
|
I think #11609 fixes the build error here. Feel free to cherry-pick. |
|
bors merge |
These will be caught by the linter in a future lean version.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
These will be caught by the linter in a future lean version.
These will be caught by the linter in a future lean version.
These will be caught by the linter in a future lean version.
These will be caught by the linter in a future lean version.
These will be caught by the linter in a future lean version.
These will be caught by the linter in a future lean version.