summaryrefslogtreecommitdiff
path: root/tests/fstar (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Regenerate test outputAymeric Fromherz2024-05-319-36/+961
|
* Implement two phases of loops join + collapseAymeric Fromherz2024-05-309-961/+36
|
* Tweak a pathNadrieril2024-05-2421-437/+437
|
* Remove secondary betree testNadrieril2024-05-248-2082/+0
| | | | | Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to add a more adequate replacement test.
* Bump charon versionNadrieril2024-05-235-7/+7
|
* Update charonNadrieril2024-04-302-2/+2
|
* Update the decreases clauses for the betreeSon Ho2024-04-262-8/+3
|
* Update the F* clauses for the betreeSon Ho2024-04-261-2/+1
|
* Update a decreases clauseSon Ho2024-04-261-1/+7
|
* Regenerate and fix the testsSon Ho2024-04-2513-23/+71
|
* Merge branch 'main' into core-option-unwrapSon Ho2024-04-2512-56/+645
|\
| * Regenerate the Primitives filesSon Ho2024-04-257-0/+525
| |
| * Update the tests for ExternalSon Ho2024-04-255-62/+120
| |
* | Update testsZyad Hassan2024-04-243-18/+0
|/
* Bump charonNadrieril2024-04-171-157/+56
|
* Fix some F* proofsSon Ho2024-04-111-4/+4
|
* Regenerate the test filesSon Ho2024-04-0422-669/+639
|
* Regenerate the test filesSon Ho2024-04-042-12/+12
|
* Regenerate the test filesSon Ho2024-04-0415-109/+109
|
* Regenerate the codeSon Ho2024-03-2011-192/+193
|
* Regenerate the testsSon Ho2024-03-197-51/+24
|
* Update the demoSon Ho2024-03-191-10/+35
|
* Regenerate the test filesSon Ho2024-03-182-22/+91
|
* Regenerate the constants tests and update Primitives/Base.leanSon Ho2024-03-181-18/+32
|
* Regenerate the test filesSon Ho2024-03-118-89/+82
|
* Update the generated filesSon Ho2024-03-115-117/+120
|
* Regenerate the test filesSon Ho2024-03-096-0/+173
|
* Add some demo filesSon Ho2024-02-093-0/+1035
|
* Fix minor issuesSon Ho2024-02-031-5/+5
|
* Rename and regenerate some filesSon Ho2024-02-026-127/+127
|
* Regenerate the filesSon Ho2024-01-255-81/+104
|
* Regenerate the filesSon Ho2023-12-2310-105/+58
|
* Improve the micro passes to eliminate pattern `let f := fun x => g x`Son Ho2023-12-231-17/+8
|
* Regenerate the test files and add the fstar-split testsSon Ho2023-12-2226-6691/+1708
|
* Regenerate some of the NoNestedBorrows testsSon Ho2023-12-222-275/+213
|
* Regenerate the test filesSon Ho2023-12-138-61/+99
|
* Regenerate the testsSon Ho2023-12-072-6/+35
|
* Update following changes in CharonSon Ho2023-12-055-119/+175
|
* Regenerate the other filesSon Ho2023-11-297-56/+1113
|
* Generate the Bitwise test filesSon Ho2023-11-291-0/+32
|
* Regenerate the testsSon Ho2023-11-292-31/+41
|
* Regenerate the test filesSon Ho2023-11-291-5/+0
|
* Generate a dedicated file for the external typesSon Ho2023-11-278-11/+43
|
* Update the generation of files for external definitions and regenerate the testsSon Ho2023-11-278-8/+8
|
* Regenerate the filesSon Ho2023-11-241-8/+2
|
* Regenerate the test filesSon Ho2023-11-221-44/+62
|
* Regenerate the filesSon Ho2023-11-211-17/+19
|
* Regenerate the filesSon Ho2023-11-2129-622/+1244
|
* Regenerate the betree filesSon Ho2023-11-218-158/+163
|
* Regenerate the Traits filesSon Ho2023-11-211-59/+62
|