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.

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

feat: deprecated find, fold, foldM, mergeBy functions for the tree map #7036

Merged
merged 8 commits into from
Feb 13, 2025

Conversation

datokrat
Copy link
Contributor

@datokrat datokrat commented Feb 11, 2025

This PR adds some deprecated function aliases to the tree map in order to ease the transition from the RBMap to the tree map.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 11, 2025 16:26 Inactive
@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 Feb 11, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 11, 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 0f1133fe69caddf47b5d3766888da929513917af --onto befee896b38349a51dad1627360adbab317f3192. (2025-02-11 16:46:59)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0f1133fe69caddf47b5d3766888da929513917af --onto 07b0e5b7fe596178282214a5c29f42e555bba59b. (2025-02-13 09:40:41)

@datokrat datokrat changed the title add deprecated find, fold and foldRev methods add deprecated find, fold and foldM methods Feb 12, 2025
@datokrat datokrat changed the title add deprecated find, fold and foldM methods feat: deprecated find, fold and foldM methods for the tree map Feb 12, 2025
@datokrat datokrat changed the title feat: deprecated find, fold and foldM methods for the tree map feat: deprecated find, fold, foldM, mergeBy methods for the tree map Feb 12, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 12, 2025 07:27 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 12, 2025 07:47 Inactive
@datokrat datokrat changed the title feat: deprecated find, fold, foldM, mergeBy methods for the tree map feat: deprecated find, fold, foldM, mergeBy functions for the tree map Feb 12, 2025
@datokrat
Copy link
Contributor Author

Cannot rebase on a nightly yet because this PR builds on top of the freshly merged tree map PR from yesterday. Will rebase as soon as possible

@datokrat datokrat marked this pull request as ready for review February 12, 2025 10:12
@datokrat datokrat requested a review from TwoFX as a code owner February 12, 2025 10:12
@datokrat datokrat added the changelog-library Library label Feb 12, 2025
Copy link
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.

LGTM. Presumably you could have got away with fewer aliases since switching from Lean.RBMap to Std.DTreeMap shouldn't happen, but no harm in having the aliases.

src/Std/Data/DTreeMap/Basic.lean Outdated Show resolved Hide resolved
src/Std/Data/DTreeMap/Basic.lean Outdated Show resolved Hide resolved
@datokrat
Copy link
Contributor Author

LGTM. Presumably you could have got away with fewer aliases since switching from Lean.RBMap to Std.DTreeMap shouldn't happen, but no harm in having the aliases.

There's Lake.Util.DRBMap, although I'm not sure whether external users would rely on that.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 12, 2025 11:55 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 13, 2025 09:27 Inactive
@datokrat datokrat added this pull request to the merge queue Feb 13, 2025
Merged via the queue into master with commit 6ac530a Feb 13, 2025
15 checks passed
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.

3 participants