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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - golf: replace some `apply foo.mpr` by `rw [foo]` #11515

Closed

grunweg wants to merge 2 commits into master from MR-rw-golf

Collaborator

grunweg commented Mar 19, 2024 •

edited

Sometimes, that line can be golfed into the next line.
Inspired by a comment of @loefflerd; any decisions are my own.

(I'm happy to drop some of these changes if they're actually dubious.)

grunweg added the WIP label


          Try a few golfs.

dc49269

grunweg force-pushed the MR-rw-golf branch from 03aad04 to dc49269 Compare

March 19, 2024 22:36

Collaborator Author

grunweg commented Mar 19, 2024

!bench

Collaborator

leanprover-bot commented Mar 19, 2024

Here are the benchmark results for commit dc49269.
There were no significant changes against commit 119c442.

grunweg changed the title ~~Try a few golfs.~~ golf: replace some apply foo.mpr by rw [foo]

grunweg marked this pull request as ready for review

March 20, 2024 10:20

grunweg added awaiting-review and removed WIP labels

fpvandoorn approved these changes

View reviewed changes

Member

fpvandoorn left a comment

I think all of these are an improvement.
I have two minor suggestions (if they compile).

bors d+

Mathlib/Control/Functor/Multivariate.lean Outdated Show resolved Hide resolved

Mathlib/Data/Set/Intervals/Disjoint.lean Outdated Show resolved Hide resolved

mathlib-bors bot commented Mar 20, 2024

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

leanprover-community-mathlib4-bot added delegated and removed awaiting-review labels


          Suggestions from code review.

56ff16d

Collaborator Author

grunweg commented Mar 20, 2024

Thank you for the fast review. Both suggestions compile.
bors r+

mathlib-bors bot pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

fa3a2fd

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

mathlib-bors bot commented Mar 20, 2024

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~golf: replace some apply foo.mpr by rw [foo]~~ [Merged by Bors] - golf: replace some apply foo.mpr by rw [foo]

mathlib-bors bot closed this

mathlib-bors bot deleted the MR-rw-golf branch

March 20, 2024 15:20

dagurtomas pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

0861c66

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

utensil pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

0a294ef

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

Louddy pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

atarnoam pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

886633a

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

uniwuni pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

b51fd9e

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

callesonne pushed a commit that referenced this pull request


          golf: replace some apply foo.mpr by rw [foo] (#11515)

453f817

Sometimes, that line can be golfed into the next line.
Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment