summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #238 from RaitoBezarius/prop-has-imp-sortSon HO2024-06-131-1/+1
|\ | | | | feat: `PropHasImp` can have `Sort u` as premisses
| * Merge branch 'main' into prop-has-imp-sortSon HO2024-06-125-45/+118
| |\ | |/ |/|
* | Merge pull request #241 from AeneasVerif/son/tacticsSon HO2024-06-125-45/+118
|\ \ | | | | | | Do minor improvements to the Lean backend
| * | Revert "Update the scalar notation for the Lean backend"Son Ho2024-06-122-26/+26
| | | | | | | | | | | | This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
| * | Revert "Regenerate the tests"Son Ho2024-06-1212-333/+338
| | | | | | | | | | | | This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.
| * | Revert "Update CoreConvertNum.lean"Son Ho2024-06-121-22/+22
| | | | | | | | | | | | This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb.
| * | Revert "Fix some mistakes"Son Ho2024-06-124-17/+15
| | | | | | | | | | | | This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd.
| * | Fix some mistakesSon Ho2024-06-124-15/+17
| | |
| * | Update CoreConvertNum.leanSon Ho2024-06-121-22/+22
| | |
| * | Regenerate the testsSon Ho2024-06-1212-338/+333
| | |
| * | Update the scalar notation for the Lean backendSon Ho2024-06-122-26/+26
| | |
| * | Deactivate the coercion from Nat to ScalarSon Ho2024-06-122-0/+17
| | |
| * | Slightly simplify the progress tacticSon Ho2024-06-121-8/+4
| | |
| * | Add wrappers around the rewriterSon Ho2024-06-121-0/+61
| | |
| * | Add the Simp.Config to the simp wrappersSon Ho2024-06-124-37/+36
|/ /
| * feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa2024-06-111-1/+1
|/ | | | | | | This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Merge pull request #237 from AeneasVerif/son/tuplesSon HO2024-06-116-28/+96
|\ | | | | Do not use tuple projectors in the Lean backend
| * Deactivate the use of tuple projectors in the Lean backendSon Ho2024-06-113-7/+12
| |
| * Update the tests for tuplesSon Ho2024-06-114-22/+85
|/
* Merge pull request #232 from Nadrieril/type-aliasGuillaume Boisseau2024-06-067-12/+56
|\
| * Filter out type aliasesNadrieril2024-06-067-12/+56
|/
* Merge pull request #233 from AeneasVerif/son/borrow-checkSon HO2024-06-0645-759/+1500
|\ | | | | Add a `-borrow-check` option
| * Regenerate the Coq and Lean betreesSon Ho2024-06-052-178/+423
| |
| * Fix a minor issueSon Ho2024-06-051-0/+1
| |
| * Update the F* betreeSon Ho2024-06-053-144/+280
| |
| * Fix a minor issueSon Ho2024-06-051-0/+1
| |
| * Update the betreeSon Ho2024-06-051-99/+98
| |
| * Regenerate some testsSon Ho2024-06-051-14/+2
| |
| * Add some negative tests for the borrow checkerSon Ho2024-06-052-0/+105
| |
| * Update an error messageSon Ho2024-06-051-6/+10
| |
| * Add more testsSon Ho2024-06-055-0/+79
| |
| * Update the test runnerSon Ho2024-06-051-1/+4
| |
| * Relax more checks for borrow-checkingSon Ho2024-06-051-1/+2
| |
| * Relax some constraints in the symbolic execution when borrow-checkingSon Ho2024-06-054-16/+54
| |
| * Update the test runner to allow the syntax [!lean] and [borrow-check]Son Ho2024-06-0514-34/+65
| |
| * Implement a BorrowCheck.borrow_check_crateSon Ho2024-06-056-10/+54
| |
| * Add an option to run Aeneas as a borrow checkerSon Ho2024-06-0510-276/+342
|/
* Merge pull request #227 from AeneasVerif/son/clean-synthesisSon HO2024-06-0515-423/+345
|\ | | | | Remove the use of `Option` from the functions synthesizing the symbolic AST
| * Merge branch 'main' into son/clean-synthesisSon Ho2024-06-0562-1437/+2425
| |\ | |/ |/|
* | Merge pull request #231 from Nadrieril/bump-haxGuillaume Boisseau2024-06-0529-291/+282
|\ \
| * | Update charonNadrieril2024-06-0529-291/+282
|/ /
* | Propagated changes to statement from Charon (#223)Escherichia2024-06-044-5/+6
| | | | | | | | | | Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Nadrieril <nadrieril+git@gmail.com>
* | Merge pull request #228 from AeneasVerif/son/loops2Son HO2024-06-0431-1149/+2143
|\ \ | | | | | | Add support for projection markers when joining environments
| * \ Merge branch 'main' into son/loops2Son Ho2024-06-04188-5984/+2764
| |\ \ | |/ / |/| |
* | | Merge pull request #230 from W95Psp/follow-up-charon-pr-209Guillaume Boisseau2024-06-047-6/+12
|\ \ \
| * | | Fix the CI pin checkNadrieril2024-06-041-0/+2
| | | |
| * | | Update charon pinNadrieril2024-06-042-4/+4
| | | |
| * | | feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209Lucas Franceschino2024-06-034-2/+6
|/ / /
| * | Improve collapse_ctxSon Ho2024-06-041-1/+42
| | |
| * | Do more cleanupSon Ho2024-06-041-40/+44
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 15:06:02 +0000