Skip to content

feat: add cbv_eval attribute#12296

Merged
wkrozowski merged 23 commits intoleanprover:masterfrom
wkrozowski:wojciech/cbv_theorems
Feb 10, 2026
Merged

feat: add cbv_eval attribute#12296
wkrozowski merged 23 commits intoleanprover:masterfrom
wkrozowski:wojciech/cbv_theorems

Conversation

@wkrozowski
Copy link
Contributor

@wkrozowski wkrozowski commented Feb 3, 2026 •
edited
Loading

This PR adds cbv_eval attribute that allows to evaluate functions in cbv tactic using pre-registered theorems.

@wkrozowski wkrozowski added the changelog-tactics User facing tactics label Feb 3, 2026
@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 3, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 5, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 96ef09186f1cfe31bf5af69adb6ead4fad218ced --onto 5ec3b8c9d2fed98e6d78782664dd545785e868d4. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-05 11:30:29)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 96ef09186f1cfe31bf5af69adb6ead4fad218ced --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-06 16:45:23)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5ba467d920da2d093676024cbca38a5525abd517 --onto 39c26fce1da321b24eaf949d0d7d028ba589e4e1. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-09 15:17:30)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 5, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 96ef09186f1cfe31bf5af69adb6ead4fad218ced --onto 42a0e9245300da6b3d971fa0033d726bb8e11cc3. You can force reference manual CI using the force-manual-ci label. (2026-02-05 11:30:31)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 96ef09186f1cfe31bf5af69adb6ead4fad218ced --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-06 16:45:26)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5ba467d920da2d093676024cbca38a5525abd517 --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-09 15:17:31)

@wkrozowski wkrozowski mentioned this pull request Feb 5, 2026
Merged
@wkrozowski wkrozowski changed the title [draft] feat: add cbv_eval attribute feat: add cbv_eval attribute Feb 5, 2026
github-merge-queue bot pushed a commit that referenced this pull request Feb 5, 2026
@wkrozowski
feat: make Theorem an Inhabited instance (#12324)
5345db8 
This PR adds a default `Inhabited` instance to `Theorem` type.

The need to do so came up in #12296 , as `Theorem` is one of the entries
of the structure which is the key entry of `SimpleScopedEnvExtension`.
nomeata
nomeata reviewed Feb 5, 2026
View reviewed changes
Copy link
Collaborator

@nomeata nomeata left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some comments

@wkrozowski wkrozowski marked this pull request as ready for review February 9, 2026 18:18
@wkrozowski wkrozowski requested review from nomeata and removed request for leodemoura February 9, 2026 18:19
nomeata
nomeata reviewed Feb 10, 2026
View reviewed changes
@wkrozowski wkrozowski enabled auto-merge February 10, 2026 15:38
@wkrozowski wkrozowski added this pull request to the merge queue Feb 10, 2026
Merged via the queue into leanprover:master with commit 7d32030 Feb 10, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@nomeata nomeata nomeata left review comments

Assignees

No one assigned

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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@wkrozowski @leanprover-bot @nomeata