Skip to content

feat: @[grind] annotations for TreeMap #8446

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
Merged
kim-em merged 10 commits into from
May 24, 2025
Merged

feat: @[grind] annotations for TreeMap #8446

kim-em merged 10 commits into from
May 24, 2025

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented May 23, 2025

This PR adds basic @[grind] annotations for TreeMap and its variants. Likely more annotations will be added after we've explored some examples.

@kim-em kim-em requested review from TwoFX and digama0 as code owners May 23, 2025 00:36
@kim-em kim-em added the changelog-library Library label May 23, 2025
@kim-em kim-em enabled auto-merge May 23, 2025 00:37
@kim-em kim-em added this pull request to the merge queue May 23, 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 May 23, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 23, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 44ff70020d4716f57afe82830cd0211a98417f38 --onto 4eccb5b4792c270ad10ac059b9672a8845961079. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-23 05:08:55)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7b80cd24a924dd1aef9d546e501daee6a777a044 --onto 4eccb5b4792c270ad10ac059b9672a8845961079. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-24 04:41:50)

@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks May 23, 2025
@kim-em kim-em added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label May 24, 2025
@kim-em kim-em added this pull request to the merge queue May 24, 2025
Merged via the queue into master with commit 38ca310 May 24, 2025
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

Assignees

No one assigned

Labels

changelog-library Library merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kim-em @leanprover-community-bot