Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 17, 2025

No description provided.

@Kha Kha requested a review from kim-em as a code owner October 17, 2025 09:38
@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 Oct 17, 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 dc7c184ee287ed4ad8fd19165349965cd85d1977 --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-17 10:37:55)

@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 dc7c184ee287ed4ad8fd19165349965cd85d1977 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-17 10:37:57)

@Kha Kha added this pull request to the merge queue Oct 17, 2025
Merged via the queue into leanprover:master with commit 5800ce1 Oct 17, 2025
17 checks passed
@Kha Kha deleted the push-zzksmpvrvmrv branch October 17, 2025 19:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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