Skip to content

feat: Thunk is inhabited#12469

Merged
Vtec234 merged 1 commit intoleanprover:masterfrom
JovanGerb:Jovan-Inhabited_Thunk
Mar 19, 2026
Merged

feat: Thunk is inhabited#12469
Vtec234 merged 1 commit intoleanprover:masterfrom
JovanGerb:Jovan-Inhabited_Thunk

Conversation

@JovanGerb
Copy link
Copy Markdown
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
Copy Markdown
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
Copy Markdown

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
Copy Markdown
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
Copy Markdown
Contributor Author

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

@nomeata
Copy link
Copy Markdown
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.

@Vtec234
Copy link
Copy Markdown
Member

Vtec234 commented Mar 19, 2026

Mathlib build succeeded here: #12991.

@Vtec234 Vtec234 added this pull request to the merge queue Mar 19, 2026
Merged via the queue into leanprover:master with commit 518a135 Mar 19, 2026
32 of 33 checks passed
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.

4 participants