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

chore: move RBNode depth lemmas out #744

Merged
merged 3 commits into from May 13, 2024
Merged

chore: move RBNode depth lemmas out #744

merged 3 commits into from May 13, 2024

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Apr 16, 2024

These lemmas are separate from the rest and need not be pulled in by the main file.

@digama0 digama0 force-pushed the rbmap_depth branch 2 times, most recently from e905481 to c406d56 Compare April 16, 2024 15:23
@digama0 digama0 added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Apr 16, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 17, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 17, 2024
@semorrison semorrison added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Apr 18, 2024
@digama0 digama0 added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Apr 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 7, 2024
@semorrison
Copy link
Collaborator

Merged main.

@semorrison semorrison merged commit 9e1609d into main May 13, 2024
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@digama0 @semorrison @leanprover-community-mathlib4-bot