summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/NoNestedBorrows.fst (unfollow)
Commit message (Expand)AuthorFilesLines
2023-11-21Regenerate most of the test filesSon Ho1-1/+4
2023-11-08Update the Makefile and regenerate some testsSon Ho1-0/+12
2023-10-27Regenerate some of the F* test filesSon Ho1-137/+129
2023-08-08Regenerate the test filesSon Ho1-6/+6
2023-07-06Improve the generated commentsSon Ho1-55/+57
2023-06-04Start updating simplify_aggregatesSon Ho1-4/+4
2023-06-04Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho1-32/+45
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-150/+70
2023-02-03Regenerate the filesSon Ho1-41/+12
2022-11-14Regenerate the files and fix the proofsSon Ho1-70/+85
2022-11-14Make good progress on the Coq backendSon Ho1-53/+0
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-0/+0
2022-11-11Make minor modifications to the tests and regenerate the .fst filesSon Ho1-10/+10
2022-05-15Regenerate the F* filesSon Ho1-23/+26
2022-05-15Treat integer casts in a general mannerSon Ho1-0/+4
2022-05-15Regenerate a test fileSon Ho1-6/+8
2022-05-06Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho1-1/+1
2022-05-01Regenerate some of the test filesSon Ho1-5/+6
2022-04-21Regenerate the test filesSon Ho1-10/+8
2022-04-20Regenerate the test filesSon Ho1-17/+17
2022-04-20Update the evaluation of matches for the cases where the scrutinee is aSon Ho1-0/+14
2022-04-20Regenerate a test fileSon Ho1-0/+20
2022-02-23Improve variable name generationSon Ho1-8/+8
2022-02-23Inline more let-bindings and improve formattingSon Ho1-24/+18
2022-02-23Track the generated F* files from tests/miscSon Ho1-0/+526
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 16:25:48 +0000