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(*): use sq as convention for "squared" #7368

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - chore(*): use sq as convention for "squared" #7368

wants to merge 9 commits into from

Conversation

benjamindavidson
Copy link
Collaborator

This PR establishes sq x as the notation for x ^ 2. See this Zulip conversation.

A breakdown of the refactor:

  • All instances of square and sqr are changed to sq (except where square means something other than "to the second power")
  • All instances of pow_two are changed to sq, though many are kept are aliases
  • All instances of sum_of_two_squares are changed to sq_add_sq

n.b. I did NOT alter any instances of:

  • squarefree
  • sum_of_four_squares
  • fpow_two or rpow_two

@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Apr 26, 2021
@semorrison
Copy link
Collaborator

bors d+

@bors
Copy link

bors bot commented Apr 27, 2021

✌️ 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.

@github-actions github-actions bot 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 Apr 27, 2021
@eric-wieser
Copy link
Member

bors r+

Since this has a high potential for conflicts, lets kick this on the queue now.

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Apr 27, 2021
@bryangingechen
Copy link
Collaborator

Unfortunately, this already has a merge conflict.
bors r-

When merging again we should use a priority, like bors r+ p=30 or something.
bors d+

@bors
Copy link

bors bot commented Apr 27, 2021

✌️ 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.

@bors
Copy link

bors bot commented Apr 27, 2021

Canceled.

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 27, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 28, 2021
@benjamindavidson
Copy link
Collaborator Author

I'm not sure what's causing the build to fail.

@benjamindavidson benjamindavidson removed the awaiting-author A reviewer has asked the author a question or requested changes label Apr 28, 2021
@eric-wieser
Copy link
Member

It's https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/elan.20is.20broken.20atm/near/236473065

@eric-wieser eric-wieser mentioned this pull request Apr 28, 2021
Closed
1 task
@bryangingechen
Copy link
Collaborator

I did a brief scan of the other PRs in the queue and it seems like it should be safe to add this to the next one. 🤞
bors r+

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 28, 2021
@benjamindavidson
Copy link
Collaborator Author

Okay. I had been waiting because I was concerned that if I add it with priority it would cancel the other PRs it is currently running but if you think this will work then great!

@bryangingechen bryangingechen mentioned this pull request Apr 28, 2021
Closed
bors bot pushed a commit that referenced this pull request Apr 28, 2021
@benjamindavidson @eric-wieser
chore(*): use sq as convention for "squared" (#7368)
b9c80c9 
This PR establishes `sq x` as the notation for `x ^ 2`. See [this Zulip conversation](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/sqr.20vs.20sq.20vs.20pow_two/near/224972795).

A breakdown of the refactor:
- All instances of `square` and `sqr` are changed to `sq` (except where `square` means something other than "to the second power")
- All instances of `pow_two` are changed to `sq`, though many are kept are aliases
- All instances of `sum_of_two_squares` are changed to `sq_add_sq`

n.b. I did NOT alter any instances of:
- `squarefree`
- `sum_of_four_squares`
- `fpow_two` or `rpow_two`


<!-- The text above the `

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Apr 29, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): use sq as convention for "squared" [Merged by Bors] - chore(*): use sq as convention for "squared" Apr 29, 2021
@bors bors bot closed this Apr 29, 2021
@bors bors bot deleted the to_sq branch April 29, 2021 00:50
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Apr 29, 2021
Closed
@bryangingechen bryangingechen mentioned this pull request Apr 30, 2021
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

@jsm28 jsm28 jsm28 left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@benjamindavidson @semorrison @eric-wieser @bryangingechen @jsm28