summaryrefslogtreecommitdiff
path: root/tests/lean/HashmapMain/Funs.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-23Regenerate the filesSon Ho1-6/+5
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-351/+252
2023-11-24Regenerate the filesSon Ho1-19/+19
2023-11-21Regenerate the filesSon Ho1-40/+80
2023-11-21Regenerate most of the test filesSon Ho1-58/+57
2023-10-26Fix some issues and regenerate the HashmapMain example for LeanSon Ho1-98/+128
2023-09-07Regenerate the test files and fix a proofSon Ho1-5/+1
2023-08-09Update the nix flake and regenerate the codeSon Ho1-1/+1
2023-08-04Make minor modificationsSon Ho1-2/+2
2023-08-03Make a minor formatting modification for LeanSon Ho1-0/+1
2023-07-12Make the `by inlit` implicitSon Ho1-51/+35
2023-07-06Use short names for the structure fields in LeanSon Ho1-76/+40
2023-07-06Improve the generated commentsSon Ho1-135/+141
2023-07-05Simplify the names used in Primitives.leanSon Ho1-33/+31
2023-07-05Simplify the generated names for the types in LeanSon Ho1-118/+114
2023-07-05Start using namespaces in the Lean backendSon Ho1-112/+109
2023-07-04Regenerate the Lean test filesSon Ho1-14/+17
2023-07-04Reorganize the Lean testsSon Ho1-85/+52
2023-06-04Regenerate the translated files for LeanSon Ho1-108/+97
2023-06-04Improve the generation of variant names for LeanSon Ho1-57/+45
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho1-51/+18
2023-06-04Start updating simplify_aggregatesSon Ho1-8/+14
2023-06-04Update the extraction of Lean filesSon Ho1-8/+15
2023-06-04Make minor modifications and regenerate the Lean filesSon Ho1-15/+8
2023-06-04WIPJonathan Protzenko1-198/+180
2023-06-04Idiomatic naming conventionsJonathan Protzenko1-210/+235
2023-06-04Improve formatting further by removing useless spacesSon Ho1-14/+0
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho1-2/+4
2023-06-04Improve formatting of the termination_by clausesSon Ho1-19/+13
2023-06-04Make minor fixes, improve formatting for Lean and generate code for all the t...Son Ho1-124/+117
2023-06-04All of the generated code is syntactically correctJonathan Protzenko1-2/+2
2023-06-04WIPJonathan Protzenko1-3/+5
2023-06-04Fix runaway indentationJonathan Protzenko1-451/+440
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko1-2/+2
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 Protzenko1-443/+451
2023-06-04WIP lots of stuffJonathan Protzenko1-13/+42
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 Protzenko1-89/+84
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko1-266/+309
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko1-108/+103
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko1-2/+2
2023-06-04Add a sample test to illustrate potential project structureJonathan Protzenko1-0/+535
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 11:24:13 +0000