index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tests
/
lean
/
hashmap_on_disk
/
HashmapMain
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Reorganize the Lean tests
Son Ho
2023-07-04
6
-851
/
+0
|
*
Regenerate the translated files for Lean
Son Ho
2023-06-04
6
-145
/
+137
|
*
Improve the generation of variant names for Lean
Son Ho
2023-06-04
2
-59
/
+47
|
*
Improve simplify_aggregates to introduce structure updates
Son Ho
2023-06-04
1
-51
/
+18
|
*
Start updating simplify_aggregates
Son Ho
2023-06-04
1
-8
/
+14
|
*
Make minor modifications to the Lean files
Son Ho
2023-06-04
1
-2
/
+1
|
*
Update the extraction of Lean files
Son Ho
2023-06-04
3
-18
/
+27
|
*
Update the generation of termination and decreases_by templates for Lean
Son Ho
2023-06-04
1
-9
/
+9
|
*
Make minor modifications and regenerate the Lean files
Son Ho
2023-06-04
2
-20
/
+12
|
*
WIP
Jonathan Protzenko
2023-06-04
1
-198
/
+180
|
*
Idiomatic naming conventions
Jonathan Protzenko
2023-06-04
4
-221
/
+247
|
*
Improve formatting further by removing useless spaces
Son Ho
2023-06-04
1
-14
/
+0
|
*
Make sure let-bindings in Lean end with line breaks and improve formatting
Son Ho
2023-06-04
1
-2
/
+4
|
*
Improve formatting of the termination_by clauses
Son Ho
2023-06-04
1
-19
/
+13
|
*
Make minor fixes, improve formatting for Lean and generate code for all the ↵
Son Ho
2023-06-04
3
-129
/
+232
|
|
|
|
test suite
*
All of the generated code is syntactically correct
Jonathan Protzenko
2023-06-04
2
-3
/
+3
|
*
WIP
Jonathan Protzenko
2023-06-04
4
-14
/
+129
|
*
Fix runaway indentation
Jonathan Protzenko
2023-06-04
1
-451
/
+440
|
*
Fill out more of the primitives file, attempt at type classes for scalar_cast
Jonathan Protzenko
2023-06-04
1
-2
/
+2
|
*
Don't need extra variables for the decreases clauses
Jonathan Protzenko
2023-06-04
1
-11
/
+15
|
*
WIP printing proper clauses
Jonathan Protzenko
2023-06-04
1
-35
/
+49
|
*
Fix some printing bits, proper syntax for terminates and decreases clauses
Jonathan Protzenko
2023-06-04
1
-443
/
+451
|
*
WIP lots of stuff
Jonathan Protzenko
2023-06-04
2
-18
/
+42
|
*
Fix a syntax error
Jonathan Protzenko
2023-06-04
1
-10
/
+5
|
*
Custom syntax support for structures in Lean
Jonathan Protzenko
2023-06-04
1
-22
/
+71
|
*
More cosmetic improvements
Jonathan Protzenko
2023-06-04
1
-89
/
+84
|
*
Fix a couple bugs here and there, improve Lean code-gen, still WIP
Jonathan Protzenko
2023-06-04
1
-266
/
+309
|
*
New directory structure and corresponding extraction, + misc fixes, for Lean
Jonathan Protzenko
2023-06-04
3
-0
/
+569