Skip to content
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] - chore(Analysis): fix mathlib3 names; automated fixes #11950

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(Analysis): fix mathlib3 names; automated fixes #11950

wants to merge 4 commits into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Apr 6, 2024

Open in Gitpod

@grunweg grunweg added documentation Improvements or additions to documentation awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) labels Apr 6, 2024
@grunweg
Copy link
Collaborator Author

grunweg commented Apr 6, 2024 •
edited

Looking over the diff:

  • I understand where the exp -> NormedSpace.exp change comes from; I'm not sure if it's actually better. Happy to revert those manually.
  • False negative (i.e. my script missed this, so far): continuous_linear_map.adjoint should also be pointed out

Update: I went over the first point and reverted the changes I dislike; and manually fixed the second one.

@grunweg grunweg marked this pull request as ready for review April 6, 2024 17:49
@grunweg grunweg force-pushed the MR-analysis-fix-mathlib3-names branch from 91339a6 to e349eb9 Compare April 6, 2024 17:56
@grunweg
Revert some of the exp changes.
bf83542 
Others are actually good, in my opinion; fix the line length there.
@grunweg
One missed one.
c5622ec
@grunweg grunweg force-pushed the MR-analysis-fix-mathlib3-names branch from e349eb9 to c5622ec Compare April 6, 2024 17:59
@kmill
Copy link
Contributor

kmill commented Apr 6, 2024

Thanks! I think NormedSpace.exp is good since it creates a link in the documentation.

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 6, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 6, 2024
@grunweg
chore(Analysis): fix mathlib3 names; automated fixes (#11950)
a8a6713
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 6, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Analysis): fix mathlib3 names; automated fixes [Merged by Bors] - chore(Analysis): fix mathlib3 names; automated fixes Apr 6, 2024
@mathlib-bors mathlib-bors bot closed this Apr 6, 2024
@mathlib-bors mathlib-bors bot deleted the MR-analysis-fix-mathlib3-names branch April 6, 2024 19:35
@grunweg
Copy link
Collaborator Author

grunweg commented Apr 7, 2024

Thank you for the fast review!

kmill
kmill reviewed Apr 7, 2024
View reviewed changes
Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
@@ -34,15 +34,15 @@ the corresponding integral, or in the proofs of its properties. We equip

The structure `BoxIntegral.IntegrationParams` has 3 boolean fields with the following meaning:

* `bRiemann`: the value `true` means that the filter corresponds to a Riemann-style integral, i.e.
* `bRiemann`: the value `True` means that the filter corresponds to a Riemann-style integral, i.e.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wasn't careful with checking True/true and False/false, sorry. These ones should be lower case.

Could you check the PRs that I merged and revert any of changes that are terms of Bool?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right... I just learned about this today. I've checked, only #11948 and this PR exhibit this issue. Hopefully, I can fix these tomorrow.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, this was easier than expected: I filed #11994 for the corrections.

Louddy pushed a commit that referenced this pull request Apr 15, 2024
@grunweg @Louddy
chore(Analysis): fix mathlib3 names; automated fixes (#11950)
4a11bc8
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@grunweg @atarnoam
chore(Analysis): fix mathlib3 names; automated fixes (#11950)
94db6ae
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@grunweg @uniwuni
chore(Analysis): fix mathlib3 names; automated fixes (#11950)
506b649
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@grunweg @callesonne
chore(Analysis): fix mathlib3 names; automated fixes (#11950)
821d503
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kmill kmill kmill left review comments

Assignees
No one assigned
Labels
documentation Improvements or additions to documentation ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@grunweg @kmill