Skip to content

Conversation

@wkrozowski
Copy link
Contributor

This PR adds support for the difference operation for ExtDHashMap/ExtHashMap/ExtHashSet and proves several lemmas about it.

@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):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-27 13:45:46)
  • ❗ 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 13:04:32)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 27, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-27 13:45:48)
  • ❗ 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 13:04:34)

@wkrozowski wkrozowski marked this pull request as ready for review December 2, 2025 14:01
@wkrozowski wkrozowski requested a review from TwoFX as a code owner December 2, 2025 14:01
@TwoFX
Copy link
Member

TwoFX commented Dec 4, 2025

@wkrozowski The GitHub diff seems to be confused here; would you mind merging master into your branch so that we don't see changes that are already merged?

@wkrozowski
Copy link
Contributor Author

@TwoFX Okay, done

@wkrozowski wkrozowski added this pull request to the merge queue Dec 4, 2025
Merged via the queue into leanprover:master with commit 42ded56 Dec 4, 2025
16 checks passed
algebraic-dev pushed a commit that referenced this pull request Dec 8, 2025
This PR adds support for the difference operation for
`ExtDHashMap`/`ExtHashMap`/`ExtHashSet` and proves several lemmas about
it.

---------

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-library Library 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