Skip to content

Conversation

@wkrozowski
Copy link
Contributor

This PR adds a difference operation on ExtDTreeMap/ExtTreeMap/TreeSet and proves several lemmas about it.

Stacked on top of #11407

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label Nov 27, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 27, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6eeb215e8f1986cd1628f8e02d6c69e337db034e --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-27 20:09:11)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 18:01:48)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e548fa414cb74db21a31afe6c26cb0c51310f1db --onto 0173444d24df9253d7947cfe82519e4a6caffd3a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 12:15:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 42ded564bd27a6ac0f64c1daf4870f67472e1f59 --onto dd28f005889dd2fcca6fe0638133de561a655ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 18:45:24)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 27, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6eeb215e8f1986cd1628f8e02d6c69e337db034e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-27 20:09:12)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-01 18:01:49)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e548fa414cb74db21a31afe6c26cb0c51310f1db --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-04 12:15:48)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 42ded564bd27a6ac0f64c1daf4870f67472e1f59 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-04 18:45:25)

@wkrozowski wkrozowski marked this pull request as ready for review December 1, 2025 15:03
@wkrozowski wkrozowski requested a review from TwoFX as a code owner December 1, 2025 15:03
@wkrozowski
Copy link
Contributor Author

@TwoFX Also merged the master here

@wkrozowski wkrozowski added this pull request to the merge queue Dec 4, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Dec 4, 2025
@wkrozowski wkrozowski added this pull request to the merge queue Dec 5, 2025
Merged via the queue into leanprover:master with commit 9cbff55 Dec 5, 2025
16 checks passed
algebraic-dev pushed a commit that referenced this pull request Dec 8, 2025
This PR adds a difference operation on
`ExtDTreeMap`/`ExtTreeMap`/`TreeSet` and proves several lemmas about it.

Stacked on top of #11407

---------

Co-authored-by: Markus Himmel <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants