Skip to content

feat(lean): Add support for nonliteral array sizes#1826

Merged
abentkamp merged 1 commit intomainfrom
lean-array-size
Dec 18, 2025
Merged

feat(lean): Add support for nonliteral array sizes#1826
abentkamp merged 1 commit intomainfrom
lean-array-size

Conversation

@abentkamp
Copy link
Copy Markdown
Contributor

Fixes #1713

@abentkamp abentkamp force-pushed the lean-array-size branch 2 times, most recently from 4bf6898 to 105d850 Compare December 17, 2025 15:31
@abentkamp abentkamp marked this pull request as ready for review December 18, 2025 08:53
@abentkamp abentkamp requested a review from a team as a code owner December 18, 2025 08:53
@abentkamp abentkamp requested review from clementblaudeau and maximebuyse and removed request for clementblaudeau December 18, 2025 08:53
@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 18, 2025
@abentkamp abentkamp added this to the Lean backend v1.0 milestone Dec 18, 2025
Copy link
Copy Markdown
Contributor

@maximebuyse maximebuyse left a comment

Choose a reason for hiding this comment

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

Great!

@abentkamp abentkamp added this pull request to the merge queue Dec 18, 2025
Merged via the queue into main with commit 6656ce3 Dec 18, 2025
17 of 18 checks passed
@abentkamp abentkamp deleted the lean-array-size branch December 18, 2025 10:38
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.

[Lean] Arrays with non-integer-literal size

2 participants