summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'main' into has-int-predSon Ho2024-06-1717-22/+22
|\
| * Merge pull request #245 from AeneasVerif/son/update-leanSon HO2024-06-176-14/+14
| |\
| | * Merge branch 'main' into son/update-leanSon Ho2024-06-171-12/+4
| | |\ | | |/ | |/|
| * | Merge pull request #249 from Nadrieril/github-ciGuillaume Boisseau2024-06-171-12/+4
| |\ \
| | * | Revert "Switch to GitHub CI runners"Nadrieril2024-06-171-12/+4
| |/ /
| | * Merge branch 'main' into son/update-leanSon Ho2024-06-171-4/+12
| | |\ | | |/ | |/|
| * | Merge pull request #248 from Nadrieril/bump-charon2Guillaume Boisseau2024-06-1717-22/+22
| |\ \
| | * | Update charonNadrieril2024-06-1717-22/+22
| |/ /
| * | Merge pull request #247 from Nadrieril/github-ciGuillaume Boisseau2024-06-171-4/+12
| |\ \
| | * | Switch to GitHub CI runnersNadrieril2024-06-171-4/+12
| |/ /
| | * Regenerate the testsSon Ho2024-06-1715-18/+18
| | * Update the Charon pinSon Ho2024-06-172-4/+4
* | | Make a minor cleanupSon Ho2024-06-171-9/+11
* | | Merge branch 'son/update-lean' into has-int-predSon Ho2024-06-1724-321/+458
|\ \ \ | | |/ | |/|
| * | Update the Lean dependenciesSon Ho2024-06-172-8/+8
| * | Update the testsSon Ho2024-06-142-4/+4
| * | 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
|\
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 07:48:42 +0000