Skip to content

feat(lean): add proof attribute#1831

Merged
W95Psp merged 6 commits intomainfrom
lean-proof
Dec 24, 2025
Merged

feat(lean): add proof attribute#1831
W95Psp merged 6 commits intomainfrom
lean-proof

Conversation

@abentkamp
Copy link
Copy Markdown
Contributor

@abentkamp abentkamp commented Dec 23, 2025 •
edited
Loading

This PR adds a hax_lib::proof attribute to specify custom Lean proofs.

@abentkamp abentkamp changed the title feat(lean): add `proof attribute feat(lean): add proof attribute Dec 23, 2025
@abentkamp abentkamp added lean Related to the Lean backend or library backend Issue in one of the backends (i.e. F*, Coq, EC...) labels Dec 23, 2025
@abentkamp abentkamp added this to the Lean backend v1.0 milestone Dec 23, 2025
W95Psp
W95Psp reviewed Dec 23, 2025
View reviewed changes
@abentkamp abentkamp changed the base branch from main to lean-int-specs December 23, 2025 15:49
@abentkamp abentkamp marked this pull request as ready for review December 23, 2025 15:58
@abentkamp abentkamp requested a review from a team as a code owner December 23, 2025 15:58
@abentkamp abentkamp requested review from clementblaudeau and removed request for a team December 23, 2025 15:58
W95Psp
W95Psp reviewed Dec 24, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

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

I'm just leaving quick notes, since @abentkamp is off, I may fix the few things I mention here (those are small things)

@karthikbhargavan
Copy link
Copy Markdown
Contributor

karthikbhargavan commented Dec 24, 2025

I'm just leaving quick notes, since @abentkamp is off, I may fix the few things I mention here (those are small things)

Yes, doing these small changes today sounds good.

Base automatically changed from lean-int-specs to main December 24, 2025 13:53
@W95Psp W95Psp added this pull request to the merge queue Dec 24, 2025
Merged via the queue into main with commit 692f0ba Dec 24, 2025
18 of 19 checks passed
@W95Psp W95Psp deleted the lean-proof branch December 24, 2025 14:26
@W95Psp W95Psp restored the lean-proof branch January 15, 2026 15:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@clementblaudeau clementblaudeau Awaiting requested review from clementblaudeau clementblaudeau is a code owner automatically assigned from cryspen/hax

1 more reviewer

@W95Psp W95Psp W95Psp approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

backend Issue in one of the backends (i.e. F*, Coq, EC...) lean Related to the Lean backend or library

Projects

None yet

Milestone

Lean backend v1.0

Development

Successfully merging this pull request may close these issues.

3 participants

@abentkamp @karthikbhargavan @W95Psp