summaryrefslogtreecommitdiff
path: root/tests/src/mutually-recursive-traits.lean.out (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Remove redundant `llbc_name` fieldNadrieril2024-06-281-6/+6
| | | | It's redundant with `item_meta.name`
* Update charonNadrieril2024-06-241-6/+6
|
* Update charonNadrieril2024-06-211-3/+3
|
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-181-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Son Ho <hosonmarc@gmail.com>
* Tiny dedupNadrieril2024-06-181-1/+1
|
* Regenerate the testsSon Ho2024-06-171-2/+2
|
* Update the test runner to allow the syntax [!lean] and [borrow-check]Son Ho2024-06-051-7/+7
|
* Remove the options from the functions synthesizing the symbolic ASTSon Ho2024-05-301-6/+6
|
* runner: Support negative testsNadrieril2024-05-271-0/+17