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] - feat(data/real/pi): Leibniz's series for pi #4228

Closed
wants to merge 35 commits into from
Closed

[Merged by Bors] - feat(data/real/pi): Leibniz's series for pi #4228

wants to merge 35 commits into from

Conversation

benjamindavidson
Copy link
Collaborator

@benjamindavidson benjamindavidson commented Sep 24, 2020 •
edited

Freek No. 26

hrmacbeth and others added 19 commits August 30, 2020 18:23
@benjamindavidson benjamindavidson added the WIP Work in progress label Sep 24, 2020
urkud
urkud reviewed Sep 24, 2020
View reviewed changes
src/data/real/pi.lean Outdated Show resolved Hide resolved
urkud
urkud reviewed Sep 24, 2020
View reviewed changes
src/data/real/pi.lean Outdated Show resolved Hide resolved
@urkud
Copy link
Member

urkud commented Sep 24, 2020

I'm sorry for leaving comments before you've requested them: somehow I saw the WIP label only after I've left the comments.

@benjamindavidson
Copy link
Collaborator Author

I'm sorry for leaving comments before you've requested them: somehow I saw the WIP label only after I've left the comments.

That's alright, I appreciate them all the same. I was aware of some of them, such as the name, placement, and questionable necessity of mvt. This PR still needs a bit of work but I hope to have it ready soon.

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 11, 2020
jcommelin
jcommelin reviewed Oct 12, 2020
View reviewed changes
src/data/real/pi.lean Outdated Show resolved Hide resolved
@benjamindavidson benjamindavidson added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 18, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 18, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 19, 2020
semorrison
semorrison approved these changes Oct 19, 2020
View reviewed changes
Copy link
Collaborator

@semorrison semorrison left a comment

Choose a reason for hiding this comment

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

LGTM

sgouezel
sgouezel reviewed Oct 19, 2020
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

lgtm, modulo minor docstring comments. You can merge yourself once these are fixed. Thanks!
bors d+

src/analysis/special_functions/pow.lean Outdated Show resolved Hide resolved
src/data/real/pi.lean Show resolved Hide resolved
@bors
Copy link

bors bot commented Oct 19, 2020

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

@semorrison semorrison added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 19, 2020
@jcommelin
Copy link
Member

@benjamindavidson If this is ready to go, then you can type bors merge or bors r+ in a comment in order to put this PR on the merge queue.

@benjamindavidson
Copy link
Collaborator Author

@benjamindavidson If this is ready to go, then you can type bors merge or bors r+ in a comment in order to put this PR on the merge queue.

Thanks, I am aware - I was just about to review my work one last time before doing exactly that.

@benjamindavidson
Copy link
Collaborator Author

IMG_6611

bors r+

bors bot pushed a commit that referenced this pull request Oct 20, 2020
@hrmacbeth @benjamindavidson
feat(data/real/pi): Leibniz's series for pi (#4228)
050b5a1 
Freek No. 26 
<!-- put comments you want to keep out of the PR commit here -->


Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
@bors
Copy link

bors bot commented Oct 20, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/real/pi): Leibniz's series for pi [Merged by Bors] - feat(data/real/pi): Leibniz's series for pi Oct 20, 2020
@bors bors bot closed this Oct 20, 2020
@bors bors bot deleted the leibniz branch October 20, 2020 08:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@robertylewis robertylewis robertylewis left review comments

@jcommelin jcommelin jcommelin left review comments

@sgouezel sgouezel sgouezel left review comments

@hrmacbeth hrmacbeth hrmacbeth left review comments

@semorrison semorrison semorrison approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
8 participants
@benjamindavidson @urkud @jcommelin @eric-wieser @semorrison @robertylewis @sgouezel @hrmacbeth