summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Bump charonNadrieril2024-06-1818-64/+64
|
* Tiny dedupNadrieril2024-06-183-13/+5
|
* Merge pull request #246 from AeneasVerif/son/cleanupSon HO2024-06-1842-508/+694
|\ | | | | Do some cleanup in the test files and the Lean backend
| * Merge branch 'main' into son/cleanupSon HO2024-06-1717-22/+22
| |\ | |/ |/|
* | Merge pull request #240 from RaitoBezarius/has-int-predSon HO2024-06-172-9/+41
|\ \ | | | | | | backends/lean: introduce `HasIntPred` automation
| * \ 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
|\ \ \ | | | | | | | | Bump Lean to 4.9.0-rc2
| * \ \ 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
|/ / / / | | | | | | | | | | | | This reverts commit dc8278e8bfd5d903ba472f6c91bd67510b23cbc4.
| * | | 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
|/ / / /
| * | | Regenerate the testsSon Ho2024-06-1715-18/+18
| | | |
| * | | Update the Charon pinSon Ho2024-06-172-4/+4
| | | |
| | | * Merge branch 'main' into son/cleanupGuillaume Boisseau2024-06-171-4/+12
| | | |\ | |_|_|/ |/| | |
* | | | 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-1726-2/+77
| | | |
| | | * Deactivate some linter options for the generated Lean filesSon Ho2024-06-171-0/+9
| | | |
| | | * Update the testsSon Ho2024-06-176-4/+31
| | | |
| | | * Automatically add a @[reducible] attribute to some generated functionsSon Ho2024-06-174-3/+66
| | | |
| | | * Update Hashmap/Properties.leanSon Ho2024-06-171-36/+34
| | | |
| | | * Update the code of the hashmapSon Ho2024-06-1712-459/+465
| | |/
| | * 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 Lean to v4.9.0-rc1
| * | 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
|\ \ | | | | | | Update the scalar notations for the Lean backend
| * | 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
|\ \ \ | | | | | | | | feat: `PropHasImp` can have `Sort u` as premisses
| * \ \ 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| | * | Merge branch 'main' into son/scalars2Son HO2024-06-120-0/+0
| | |\ \ | |_|/ / |/| | |
* | | | Merge pull request #241 from AeneasVerif/son/tacticsSon HO2024-06-125-45/+118
|\ \ \ \ | |/ / / |/| | | Do minor improvements to the Lean backend
| | * | 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
| | | | | | | | | | | | 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
| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:17:40 +0000