Skip to content

feat: @[instance_reducible] part 2 #12263

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
Open
leodemoura wants to merge 10 commits into
base: master
Choose a base branch
from
Open

feat: @[instance_reducible] part 2 #12263

leodemoura wants to merge 10 commits into from
+110 −164

Conversation

@leodemoura
Copy link
Member

@leodemoura leodemoura commented Feb 1, 2026

No description provided.

@leodemoura leodemoura requested a review from kim-em as a code owner February 1, 2026 05:46
@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 1, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 1, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ec60620534cc25d1e16612468a7d3ba80cf91938 --onto d1514f3cecc4139039962137fcf3a84c9459194a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-01 06:37:45)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 1, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ec60620534cc25d1e16612468a7d3ba80cf91938 --onto 42a0e9245300da6b3d971fa0033d726bb8e11cc3. You can force reference manual CI using the force-manual-ci label. (2026-02-01 06:37:47)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

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.

5 participants

@leodemoura @leanprover-community-bot @leanprover-bot @Kha