summaryrefslogtreecommitdiff
path: root/tests/fstar/betree/BetreeMain.Funs.fst (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Make a minor fixSon Ho1-9/+8
2023-06-04Improve simplify_aggregates to introduce structure updatesSon Ho1-48/+9
2023-06-04Start updating simplify_aggregatesSon Ho1-23/+75
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho1-60/+61
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-958/+458
2023-02-03Improve PureMicroPasses.filter_useless and regenerate the betree codeSon Ho1-12/+10
2023-02-03Regenerate the filesSon Ho1-194/+42
2022-11-16Improve formattingSon Ho1-8/+8
2022-11-14Regenerate the files and fix the proofsSon Ho1-209/+212
2022-11-14Improve the formatting of the generated codeSon Ho1-10/+8
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-0/+0
2022-10-20Regenerate the filesSon Ho1-1/+1
2022-08-11Correct assertion for stateless globalsSidney Congard1-4/+3
2022-07-05Remove last prints, adapt JSONSidney Congard1-177/+182
2022-05-15Regenerate the F* filesSon Ho1-85/+28
2022-05-09Update the termination proofs of the betreeSon Ho1-8/+8
2022-05-06Make the betree workSon Ho1-306/+306
2022-05-06Regenerate the F* files for the betreeSon Ho1-38/+73
2022-05-06Generate F* files for the betreeSon Ho1-0/+1672
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 14:27:52 +0000