Skip to content

Conversation

@srghma
Copy link

@srghma srghma commented Sep 3, 2025

This PR add Std.TreeSet.diff, Std.TreeSet.subset, SSet.subset, NameSet.diff, NameSet.subset, NameSSet.subset, SMap.any, SMap.all, SMap.subset.

Required for chasenorman/CanonicalLean#23

@srghma srghma requested a review from TwoFX as a code owner September 3, 2025 03:45
@srghma srghma changed the title feat: add Std.TreeSet.subset, SSet.subset, NameSet.subset, NameSSet.subset, SMap.any, SMap.all, SMap.subset feat: add Std.TreeSet.diff, Std.TreeSet.subset, SSet.subset, NameSet.diff, NameSet.subset, NameSSet.subset, SMap.any, SMap.all, SMap.subset Sep 3, 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 Sep 3, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a4f6f391fe27ff9a776aaf5f481b18a21e39e358 --onto d826474b14c44bad6b765c866dd4aa27307ad995. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-03 04:31:42)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a4f6f391fe27ff9a776aaf5f481b18a21e39e358 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-03 04:31:43)

…diff, NameSet.subset, NameSSet.subset, SMap.any, SMap.all, SMap.subset
@srghma srghma force-pushed the feat-add-TreeSet-subset branch from 81ae981 to df5f766 Compare September 3, 2025 04:37
@fNBU
Copy link

fNBU commented Sep 7, 2025

@srghma I think the correct label that needs to be added is changelog-language. I can't add it for you.

@srghma
Copy link
Author

srghma commented Sep 8, 2025

changelog-language

@github-actions github-actions bot added the changelog-language Language features and metaprograms label Sep 8, 2025
@srghma
Copy link
Author

srghma commented Sep 8, 2025

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Sep 8, 2025
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Sep 10, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-review Waiting for someone to review the PR changelog-language Language features and metaprograms P-medium We may work on this issue if we find the time 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