Skip to content

feat: Thunk is inhabited#12469

Open
JovanGerb wants to merge 1 commit intoleanprover:masterfrom
JovanGerb:Jovan-Inhabited_Thunk
Open

feat: Thunk is inhabited#12469
JovanGerb wants to merge 1 commit intoleanprover:masterfrom
JovanGerb:Jovan-Inhabited_Thunk

Conversation

@JovanGerb
Copy link
Contributor

This PR adds the Inhabited instance for Thunk.

We need this in batteries to call PersistentEnvExtension.getState on a state that is wrapped in a Thunk, see https://github.com/leanprover-community/batteries/pull/1667/changes.

@JovanGerb
Copy link
Contributor Author

changelog-library

@github-actions github-actions bot added changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Feb 13, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3c64f6a74934b832f9578be117052c5e29c80f39 --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 17:44:18)

@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 3c64f6a74934b832f9578be117052c5e29c80f39 --onto 9da8f5dce42832b8411d58446653f3640a94a6e3. You can force reference manual CI using the force-manual-ci label. (2026-02-13 17:44:20)

@JovanGerb
Copy link
Contributor Author

Should I just make an empty commit to make CI green, now that I've added the changelog label?

@nomeata
Copy link
Collaborator

nomeata commented Feb 14, 2026

One way to get CI to notice the label is to close and open the PR. Empty commit or force push work too.

@JovanGerb JovanGerb closed this Feb 14, 2026
@JovanGerb JovanGerb reopened this Feb 14, 2026
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