Skip to content

feat: use cbv in several examples#304

Merged
TwoFX merged 1 commit intoleanprover:masterfrom
wkrozowski:wojciech/use_cbv
Mar 26, 2026
Merged

feat: use cbv in several examples#304
TwoFX merged 1 commit intoleanprover:masterfrom
wkrozowski:wojciech/use_cbv

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

This PR changes several proofs that rely on native_decide to instead use cbv.

@wkrozowski
Copy link
Copy Markdown
Contributor Author

@TwoFX I don't think I have rights to merge to this repo. Could you have a look at it / allow me to merge things here?

Copy link
Copy Markdown
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

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

Thanks!

@TwoFX TwoFX merged commit 1d2260f into leanprover:master Mar 26, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants