Skip to content

Extensions#15

Merged
maximebuyse merged 7 commits into
mainfrom
spqr-extensions
Jun 15, 2026
Merged

Extensions#15
maximebuyse merged 7 commits into
mainfrom
spqr-extensions

Conversation

@maximebuyse

@maximebuyse maximebuyse commented Jun 4, 2026

Copy link
Copy Markdown
Collaborator

Various extensions needed for a proof project. The main decision was to switch the Vec model to take no allocator, this goes together with a change in aeneas (merged to our core-models option in cryspen/aeneas/dev)

@maximebuyse maximebuyse marked this pull request as ready for review June 8, 2026 09:48
@maximebuyse maximebuyse requested a review from abentkamp June 8, 2026 09:48

@abentkamp abentkamp left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

The solution for Vec looks great! I have a couple of comments.

Comment thread alloc/src/lib.rs Outdated
Comment thread core-models/src/core/slice.rs
Comment thread lean/CoreModels/Core/FunsEpilogue.lean Outdated
Comment thread lean/CoreModels/Core/FunsEpilogue.lean Outdated
Comment thread lean/CoreModels/Core/FunsEpilogue.lean
Comment thread lean/CoreModels/Core/FunsEpilogue.lean Outdated
Comment thread lean/CoreModels/Core/TypesPrologue.lean Outdated
@maximebuyse maximebuyse merged commit 9a0e37d into main Jun 15, 2026
3 checks 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