Skip to content

Pull requests: AeneasVerif/aeneas

New pull request New
53 Open 812 Closed
53 Open 812 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Migrate Aeneas to the Lean module system
#1230 opened Jul 24, 2026 by oliver-butterley Collaborator • Draft
Introduce ub variant for Result
#1226 opened Jul 22, 2026 by mdittmer Contributor Loading…
3
Minimize the generic parameters of globals/constants
#1224 opened Jul 20, 2026 by oliver-butterley Collaborator • Draft
1
2
Fix minor issues with nested references
#1190 opened Jul 6, 2026 by sonmarcho Member • Draft
Fix translation of nested shared borrow used in loop
#1189 opened Jul 6, 2026 by niooss-ledger Contributor Loading…
feat: Multi-file extraction.
#1185 opened Jul 2, 2026 by mpenciak Collaborator Loading…
16
Jacob/itree separation logic
#1180 opened Jul 1, 2026 by jeprinz Collaborator Loading…
1
Avoid reserved keywords being used as a bare name
#1169 opened Jun 25, 2026 by oliver-butterley Collaborator • Draft
1
Add a prepass to normalize the type of Box::new
#1167 opened Jun 25, 2026 by sonmarcho Member Loading…
Improve bind_assoc rewritings
#1156 opened Jun 23, 2026 by sonmarcho Member • Draft
1
Update get_target to output a native Lean string
#1155 opened Jun 23, 2026 by sonmarcho Member • Draft
Simplify Step.introOutputs
#1151 opened Jun 22, 2026 by sonmarcho Member • Draft
6
Deduplication of identifiers arising from traits awaiting author A reviewer has asked the author a question or requested changes.
#1142 opened Jun 20, 2026 by oliver-butterley Collaborator Loading…
1
9
Treat missing trait declaration as not builtin in trait_impl_is_builtin
#1137 opened Jun 18, 2026 by SAY-5 Loading…
1
6
Feat/range iterator next step spec
#1133 opened Jun 17, 2026 by eslerm Loading…
1
1
Fix Iterator extraction
#1131 opened Jun 17, 2026 by mpenciak Collaborator Loading…
De-duplicate parent trait names
#1128 opened Jun 16, 2026 by mpenciak Collaborator Loading…
4
Allow using expressions with #decompose
#1111 opened Jun 10, 2026 by sonmarcho Member • Draft
Support for partial mvcgen specs
#1101 opened Jun 4, 2026 by abentkamp Collaborator Loading…
Initial draft of basic float support for lean backend
#1073 opened May 28, 2026 by ezrosent • Draft
Use better names for trait impls
#1067 opened May 27, 2026 by sonmarcho Member • Draft
Fix double visit in lookup_aproj_loans_opt
#1065 opened May 27, 2026 by waamm Loading…
3
feat: Improve postcondition naming
#1058 opened May 25, 2026 by mpenciak Collaborator Loading…
Add models for DoubleEndedIterator and Rev
#1057 opened May 25, 2026 by sonmarcho Member Loading…
Annotate bare ADT constructors when Lean cannot infer their type
#1021 opened May 13, 2026 by maximebuyse Contributor Loading…
1
4
ProTip! Add no:assignee to see everything that’s not assigned.