summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Some proseJonathan Protzenko1-40/+45
2023-06-04Idiomatic naming conventionsJonathan Protzenko5-271/+297
2023-06-04Improve formatting further by removing useless spacesSon Ho5-90/+33
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho23-334/+391
2023-06-04Improve formatting of the termination_by clausesSon Ho3-84/+52
2023-06-04Make minor fixes, improve formatting for Lean and generate code for all the t...Son Ho34-175/+5431
2023-06-04Make sure Main runs some codeJonathan Protzenko1-2/+7
2023-06-04All of the generated code is syntactically correctJonathan Protzenko2-3/+3
2023-06-04WIPJonathan Protzenko6-40/+206
2023-06-04Fix runaway indentationJonathan Protzenko1-451/+440
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko2-4/+28
2023-06-04Remove last sorry in PrimitivesJonathan Protzenko1-4/+2
2023-06-04Fill out Primitives.leanJonathan Protzenko2-10/+110
2023-06-04Don't need extra variables for the decreases clausesJonathan Protzenko1-11/+15
2023-06-04WIP printing proper clausesJonathan Protzenko1-35/+49
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko2-446/+481
2023-06-04WIP lots of stuffJonathan Protzenko4-24/+73
2023-06-04Fixup one primitive that is not assumed to be monadicJonathan Protzenko1-4/+4
2023-06-04Fix a syntax errorJonathan Protzenko1-10/+5
2023-06-04Custom syntax support for structures in LeanJonathan Protzenko1-22/+71
2023-06-04More cosmetic improvementsJonathan Protzenko2-89/+85
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko2-266/+310
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko8-132/+138
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko2-8/+27
2023-06-04Add a sample test to illustrate potential project structureJonathan Protzenko9-0/+751
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-3/+4
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho15-3632/+1667
2023-02-03Update the hashmap and regenerateSon Ho9-62/+37
2023-02-03Improve the pretty names generation for loopsSon Ho6-47/+47
2023-02-03Make modifications to the MakefilesSon Ho2-6/+18
2023-02-03Implement a pass to filter the unused input arguments in the loop functionsSon Ho4-31/+22
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho10-142/+149
2023-02-03Improve the order of the loop input parametersSon Ho13-62/+62
2023-02-03Improve the heuristic to find pretty names for the variables in the loopsSon Ho9-377/+387
2023-02-03Improve PureMicroPasses.filter_useless and regenerate the betree codeSon Ho3-85/+56
2023-02-03Regenerate the hashmap code and update the proofsSon Ho10-380/+681
2023-02-03Fix some issues with the values given back by loop backward translationsSon Ho4-0/+160
2023-02-03Fix an issue with the translation of loops::clearSon Ho2-16/+6
2023-02-03Add more loop examples and fix issuesSon Ho4-0/+312
2023-02-03Implement support for nested borrows in loops, and add loop testsSon Ho4-18/+820
2023-02-03Regenerate the testsSon Ho4-0/+394
2023-02-03Improve the loops' numberingSon Ho2-19/+18
2023-02-03Make another loop example workSon Ho4-0/+44
2023-02-03Regenerate the filesSon Ho19-863/+245
2023-02-03Make minor modifications and generate code for loopsSon Ho6-0/+176
2022-11-16Add a nix derivation for the Coq proofsSon Ho2-2/+7
2022-11-16Do not introduce match on the fuel for non-recursive functionsSon Ho3-667/+477
2022-11-16Automatically generate the Makefile and _CoqProject files in the tests subdir...Son Ho16-15/+51
2022-11-16Add the aeneas-verify-fstar derivationSon Ho5-5/+10
2022-11-16Generate record field projectors for CoqSon Ho10-695/+612
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 20:52:36 +0000