summaryrefslogtreecommitdiff
path: root/tests/fstar/betree/Betree.Funs.fst (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-05Update the F* betreeSon Ho1-101/+218
2024-05-28tests: Rename betree_main -> betreeNadrieril1-44/+44
2024-04-30Update charonNadrieril1-1/+1
2024-04-25Regenerate and fix the testsSon Ho1-10/+10
2024-04-04Regenerate the test filesSon Ho1-60/+60
2024-04-04Regenerate the test filesSon Ho1-6/+6
2024-03-20Regenerate the codeSon Ho1-68/+73
2024-03-19Regenerate the testsSon Ho1-4/+2
2024-03-11Regenerate the test filesSon Ho1-8/+8
2023-12-23Regenerate the filesSon Ho1-23/+10
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-585/+260
2023-12-05Update following changes in CharonSon Ho1-16/+16
2023-11-27Update the generation of files for external definitions and regenerate the testsSon Ho1-1/+1
2023-11-21Regenerate the filesSon Ho1-56/+112
2023-11-21Regenerate the betree filesSon Ho1-58/+60
2023-10-27Regenerate more F* filesSon Ho1-592/+529
2023-09-07Regenerate the test files and fix a proofSon Ho1-6/+2
2023-08-09Update the nix flake and regenerate the codeSon Ho1-1/+1
2023-08-08Regenerate the test filesSon Ho1-217/+217
2023-07-06Improve the generated commentsSon Ho1-56/+62
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-12-26 12:34:01 +0000