Skip to content

Issues: AeneasVerif/aeneas

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

43 Open 36 Closed
43 Open 36 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Add a micro-pass to simplify array updates
#188 opened May 17, 2024 by sonmarcho
Generate projectors for recursive structs during Lean extraction
#185 opened May 15, 2024 by R1kM
@R1kM
Make the test suite standalone
#182 opened May 15, 2024 by Nadrieril
@Nadrieril
Add support for nested borrows in function signatures
#181 opened May 14, 2024 by sonmarcho
progress ... with require a context hypothesis to proceed in some cases
#179 opened May 14, 2024 by RaitoBezarius
@sonmarcho
Add support for mutually recursive trait declarations
#176 opened May 13, 2024 by sonmarcho
Add Negative Tests
#171 opened May 6, 2024 by R1kM
@Nadrieril
Do not use the Result type for functions which syntactically never fail
#161 opened Apr 26, 2024 by sonmarcho
10
Update the way spans of external definitions are printed
#160 opened Apr 25, 2024 by sonmarcho
Add a backend test for infinite loops
#153 opened Apr 22, 2024 by sonmarcho
@Nadrieril
Check in CI that the build doesn't generate warnings
#150 opened Apr 19, 2024 by sonmarcho
@Nadrieril
Add a Contributing.md file
#143 opened Apr 17, 2024 by sonmarcho
Erase unneeded Copy markers
#142 opened Apr 16, 2024 by RaitoBezarius
3
Failure when extracting a loop with a shared borrow bug Something isn't working
#134 opened Apr 16, 2024 by RaitoBezarius
@sonmarcho
1
Add String to the Lean library
#117 opened Apr 8, 2024 by zhassan-aws
Use omega instead of linarith in the scalar_tac tactic
#105 opened Apr 3, 2024 by sonmarcho
1
Make progress usable on implications
#103 opened Apr 2, 2024 by zhassan-aws
1
Crash when extracting reference to Self
#100 opened Mar 27, 2024 by sonmarcho
Register a theorem for induction over positive integers
#99 opened Mar 27, 2024 by sonmarcho
Allow types to be parameterized by traits
#98 opened Mar 26, 2024 by sonmarcho
Don't use projectors for structures extracted as tuples
#89 opened Mar 11, 2024 by sonmarcho
Add support for closures
#86 opened Mar 9, 2024 by zhassan-aws
1
Update the ways CPS is used in the compiler
#84 opened Mar 8, 2024 by sonmarcho
@EschericHya
Replace unused function inputs with _
#81 opened Mar 8, 2024 by sonmarcho
@EschericHya
Reorganize the compiler folder into subfolders
#79 opened Mar 4, 2024 by sonmarcho
ProTip! Add no:assignee to see everything that’s not assigned.