summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-23Improve the micro passes to eliminate pattern `let f := fun x => g x`Son Ho3-52/+24
2023-12-23Fix a minor issue in the Lean testsSon Ho1-14/+3
2023-12-23Update the proof of the hashmap in LeanSon Ho1-100/+44
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho106-8265/+15092
2023-12-22Annotate the bound vars in the lambdas for CoqSon Ho2-273/+231
2023-12-22Start pushing files from the fstar-split test folderSon Ho6-0/+1637
2023-12-22Regenerate some of the NoNestedBorrows testsSon Ho3-546/+474
2023-12-22Add an option to split the fwd/back functions and fix a minor issueSon Ho1-1/+1
2023-12-13Regenerate the test filesSon Ho16-183/+265
2023-12-07Regenerate the testsSon Ho6-32/+110
2023-12-05Update following changes in CharonSon Ho10-304/+476
2023-11-29Regenerate the other filesSon Ho14-56/+1570
2023-11-29Generate the Bitwise test filesSon Ho3-0/+107
2023-11-29Regenerate the testsSon Ho4-89/+125
2023-11-29Regenerate the test filesSon Ho3-15/+0
2023-11-27Generate a dedicated file for the external typesSon Ho45-78/+253
2023-11-27Update the generation of files for external definitions and regenerate the testsSon Ho20-24/+144
2023-11-24Regenerate the filesSon Ho12-282/+259
2023-11-22Regenerate the test filesSon Ho3-131/+186
2023-11-21Regenerate the filesSon Ho3-61/+71
2023-11-21Regenerate the filesSon Ho65-1578/+3156
2023-11-21Regenerate the betree filesSon Ho12-274/+279
2023-11-21Regenerate the Traits filesSon Ho3-184/+195
2023-11-21Regenerate most of the test filesSon Ho35-1016/+1045
2023-11-21Fix issues with the builtin namesSon Ho1-5/+7
2023-11-09Make administrative updates in the testsSon Ho2-405/+49
2023-11-09Update the failing proofsSon Ho13-1704/+1009
2023-11-09Regenerate the Coq test filesSon Ho14-80/+1403
2023-11-09Remove a fileSon Ho1-387/+0
2023-11-09Regenerate the testsSon Ho2-94/+37
2023-11-09Progress on making the traits work for F*Son Ho3-0/+1501
2023-11-09Modify some options and update the MakefileSon Ho8-1060/+2258
2023-11-09Regenerate some Lean testsSon Ho2-0/+39
2023-11-08Update the Makefile and regenerate some testsSon Ho3-0/+36
2023-11-07Update the extractionSon Ho2-0/+13
2023-11-06Regenerate part of the trait tests for LeanSon Ho2-16/+65
2023-10-27Add some files for the Coq trait testsSon Ho2-0/+28
2023-10-27Regenerate the Coq test filesSon Ho23-2117/+3588
2023-10-27Regenerate more F* filesSon Ho18-1549/+1427
2023-10-27Fix a minor issue and regenerate some F* test filesSon Ho9-593/+626
2023-10-27Regenerate some of the F* test filesSon Ho18-438/+530
2023-10-26Make minor modifications and update the array test for F*Son Ho3-174/+183
2023-10-26Update Primitives.fstSon Ho7-270/+2439
2023-10-26Fix some issues and regenerate the HashmapMain example for LeanSon Ho2-99/+129
2023-10-26Regenerate the betree example for LeanSon Ho1-40/+39
2023-10-26Regenerate several test files for LeanSon Ho4-122/+132
2023-10-26Regenerate the array files for LeanSon Ho2-111/+103
2023-10-25Regenerate the hashmap filesSon Ho2-86/+133
2023-10-25Regenerate the Lean array testSon Ho1-169/+150
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-6/+6