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.

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

[Merged by Bors] - chore: adapt to multiple goal linter 5 #12560

Closed
wants to merge 6 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 30, 2024

Splits off the alphabetically first half of #12381 in a separate PR to help reviewing.


Open in Gitpod

@adomani adomani changed the title chore: add 68 files from #12381 chore: adapt to multiple goal linter 4 Apr 30, 2024
@adomani adomani changed the title chore: adapt to multiple goal linter 4 chore: adapt to multiple goal linter 5 Apr 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 8, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 8, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 9, 2024
@jcommelin
Copy link
Member

bors d+

bors merge

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 11, 2024

✌️ adomani 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 ready-to-merge This PR has been sent to bors. delegated and removed awaiting-review labels May 11, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 11, 2024
Splits off the alphabetically first half of #12381 in a separate PR to help reviewing.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 11, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: adapt to multiple goal linter 5 [Merged by Bors] - chore: adapt to multiple goal linter 5 May 11, 2024
@mathlib-bors mathlib-bors bot closed this May 11, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/use_cdots_5 branch May 11, 2024 08:45
apnelson1 pushed a commit that referenced this pull request May 12, 2024
Splits off the alphabetically first half of #12381 in a separate PR to help reviewing.
mathlib-bors bot pushed a commit that referenced this pull request May 13, 2024
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560.

This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834.

A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339.

This should be the last of the adaptations.
callesonne pushed a commit that referenced this pull request May 16, 2024
Splits off the alphabetically first half of #12381 in a separate PR to help reviewing.
callesonne pushed a commit that referenced this pull request May 16, 2024
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560.

This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834.

A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339.

This should be the last of the adaptations.
grunweg pushed a commit that referenced this pull request May 17, 2024
Splits off the alphabetically first half of #12381 in a separate PR to help reviewing.
grunweg pushed a commit that referenced this pull request May 17, 2024
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560.

This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834.

A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339.

This should be the last of the adaptations.
mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
A linter that makes sure that, when multiple goals are present, they are enclosed in `·`s.

Adaptations (the order is chronological, there should be no dependency among them):
* #12338,
* #12361,
* #12372,
* #12560,
* #12834,
* #12381,
* #12908,
* #14939,

plus many many more that this comment is too small to contain.



Co-authored-by: Michael Rothgang <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants