Skip to content

Conversation

@leodemoura
Copy link
Member

This PR allows users to declare additional grind constraint propagators for declarations that already include propagators in core.

This PR allows users to declare additional `grind` constraint propagators for
declarations that already include propagators in core.
@leodemoura leodemoura added the changelog-tactics User facing tactics label Sep 26, 2025
@leodemoura leodemoura added this pull request to the merge queue Sep 26, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Sep 26, 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 27, 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 7ee3079afbdb893b124068078f654269be09a95b --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 00:28:31)

@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 7ee3079afbdb893b124068078f654269be09a95b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-27 00:28:33)

@leodemoura leodemoura added this pull request to the merge queue Sep 27, 2025
Merged via the queue into master with commit 0bf7741 Sep 27, 2025
21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics 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