summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Prove hash_map_insert_fwd_back_specSon Ho1-1/+59
2023-06-04Make progress on the proofs of the hash mapSon Ho1-4/+619
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho1-46/+686
2023-06-04Start working on the proofs of the hash mapSon Ho1-0/+543
2023-06-04Update tests/MakefileSon Ho1-1/+1
2023-06-04Add the generated HOL4 filesSon Ho43-0/+13198
2023-06-04Make good progress on generating code for HOL4Son Ho11-109/+148
2023-06-04Add Result_Inhabited to Primitives.leanSon Ho8-0/+24
2023-06-04Regenerate the translated files for LeanSon Ho37-4931/+4452
2023-06-04Make a minor fixSon Ho4-39/+32
2023-06-04Improve the generation of variant names for LeanSon Ho11-451/+419
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho7-314/+79
2023-06-04Start updating simplify_aggregatesSon Ho14-292/+589
2023-06-04Make minor modifications to the Lean filesSon Ho3-15/+14
2023-06-04Update the extraction of Lean filesSon Ho42-139/+364
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho29-0/+2357
2023-06-04Remove the tests/lean/hashmap_on_disk/Main.lean fileSon Ho1-10/+0
2023-06-04Generate all the lakefile.lean filesSon Ho6-0/+108
2023-06-04Automate the generation of the lakefile.lean filesSon Ho1-7/+3
2023-06-04Update the generation of termination and decreases_by templates for LeanSon Ho3-37/+37
2023-06-04Make minor modifications and regenerate the Lean filesSon Ho20-1488/+1599
2023-06-04WIPJonathan Protzenko2-233/+221
2023-06-04More commentsJonathan Protzenko1-0/+8
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:06:12 +0000