summaryrefslogtreecommitdiff
path: root/tests (unfollow)
Commit message (Expand)AuthorFilesLines
2024-03-18Regenerate the constants tests and update Primitives/Base.leanSon Ho3-54/+100
2024-03-11Regenerate the test filesSon Ho14-244/+227
2024-03-11Update the generated filesSon Ho15-380/+389
2024-03-11Update tests/MakefileSon Ho1-1/+1
2024-03-09Regenerate the test filesSon Ho10-0/+420
2024-03-08Remove the split test files for F*Son Ho55-16239/+0
2024-03-08Update the code generated for tuple projectorsSon Ho1-1/+1
2024-03-08Fix tuple indexing for Lean backendZyad Hassan1-1/+1
2024-03-08Update the generation of constant bodies for LeanSon Ho4-24/+23
2024-03-08Regenerate the test filesSon Ho5-46/+46
2024-02-09Remove a file which shouldn't have been addedSon Ho1-49/+0
2024-02-09Add some missing filesSon Ho4-0/+128
2024-02-09Add some demo filesSon Ho11-0/+3390
2024-02-03Fix minor issuesSon Ho2-10/+10
2024-02-02Update the .gitignore filesSon Ho1-1/+2
2024-02-02Rename and regenerate some filesSon Ho21-952/+508
2024-02-02Make progress on fixing the testsSon Ho1-13/+13
2024-02-02Start fixing the testsSon Ho7-80/+98
2024-01-25Update a decreases clauseSon Ho1-0/+5
2024-01-25Regenerate the filesSon Ho13-314/+379
2023-12-23Fix an issue in External_FunsExternal.vSon Ho1-15/+3
2023-12-23Fix an issue when deconstructing tuples in CoqSon Ho1-2/+2
2023-12-23Regenerate the filesSon Ho35-327/+183
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