Skip to content

[Merged by Bors] - chore: cleanup some simp sets#14279

Closed
kim-em wants to merge 1 commit intomasterfrom
rm_succ_eq_and_one
Closed

[Merged by Bors] - chore: cleanup some simp sets#14279
kim-em wants to merge 1 commit intomasterfrom
rm_succ_eq_and_one

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jun 30, 2024


Open in Gitpod

@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 30, 2024
@github-actions
Copy link
Copy Markdown

PR summary b36a3d0ce1

Import changes

No significant changes to the import graph


Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 30, 2024
Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

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

bors r+

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: cleanup some simp sets [Merged by Bors] - chore: cleanup some simp sets Jun 30, 2024
@mathlib-bors mathlib-bors bot closed this Jun 30, 2024
@mathlib-bors mathlib-bors bot deleted the rm_succ_eq_and_one branch June 30, 2024 07:25
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants