Skip to content

feat(lean): Allow binding of subpatterns in match constructs#1790

Merged
abentkamp merged 1 commit intomainfrom
lean-match
Dec 1, 2025
Merged

feat(lean): Allow binding of subpatterns in match constructs#1790
abentkamp merged 1 commit intomainfrom
lean-match

Conversation

@abentkamp
Copy link
Copy Markdown
Contributor

Issue #1712

@abentkamp abentkamp added this to the Lean backend v1.0 milestone Dec 1, 2025
@abentkamp abentkamp requested a review from a team as a code owner December 1, 2025 14:26
@abentkamp abentkamp added backend Issue in one of the backends (i.e. F*, Coq, EC...) lean Related to the Lean backend or library labels Dec 1, 2025
@abentkamp abentkamp requested review from clementblaudeau and maximebuyse and removed request for clementblaudeau December 1, 2025 14:26
@abentkamp abentkamp added this pull request to the merge queue Dec 1, 2025
Merged via the queue into main with commit ef7848a Dec 1, 2025
17 of 18 checks passed
@abentkamp abentkamp deleted the lean-match branch December 1, 2025 15:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants