summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
| * | Start updating Lean to 4.9.0-rc2Son Ho2024-06-142-4/+4
|/ /
* | Merge pull request #243 from AeneasVerif/son/update-leanSon HO2024-06-1318-168/+196
|\ \
| * | Update the testsSon Ho2024-06-134-34/+29
| * | Update Lean to v4.9.0-rc1Son Ho2024-06-1315-139/+172
|/ /
* | Merge pull request #242 from AeneasVerif/son/scalars2Son HO2024-06-139-114/+150
|\ \
| * | Fix more issues with the scalar notationsSon Ho2024-06-131-15/+29
| * | Fix more issuesSon Ho2024-06-133-16/+22
| * | Fix a proofSon Ho2024-06-131-1/+1
| * | Merge branch 'main' into son/scalars2Son HO2024-06-131-1/+1
| |\ \ | |/ / |/| |
* | | Merge pull request #238 from RaitoBezarius/prop-has-imp-sortSon HO2024-06-131-1/+1
|\ \ \
| * \ \ Merge branch 'main' into prop-has-imp-sortSon HO2024-06-125-45/+118
| |\ \ \ | |/ / / |/| | |
| * | | feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa2024-06-111-1/+1
| | * | Merge branch 'main' into son/scalars2Son HO2024-06-120-0/+0
| | |\ \ | |_|/ / |/| | |
* | | | Merge pull request #241 from AeneasVerif/son/tacticsSon HO2024-06-125-45/+118
|\ \ \ \ | |/ / / |/| | |
| | * | Add an exampleSon Ho2024-06-121-0/+3
| | * | Update the code extraction and regenerate the testsSon Ho2024-06-123-9/+15
| | * | Update the scalar notations in LeanSon Ho2024-06-123-102/+109
| |/ /
| * | Revert "Update the scalar notation for the Lean backend"Son Ho2024-06-122-26/+26
| * | Revert "Regenerate the tests"Son Ho2024-06-1212-333/+338
| * | Revert "Update CoreConvertNum.lean"Son Ho2024-06-121-22/+22
| * | Revert "Fix some mistakes"Son Ho2024-06-124-17/+15
| * | 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
|/ /
| * backends/lean: introduce `HasIntPred` automationRyan Lahfa2024-06-122-8/+38
|/
* Merge pull request #237 from AeneasVerif/son/tuplesSon HO2024-06-116-28/+96
|\
| * 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
|\
| * 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 19:36:35 +0000