summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2024-06-228-126/+179
* Add some proofs for the Lean backend (#255)Son HO2024-06-2118-165/+1163
* Merge pull request #254 from Nadrieril/declarationgroup-mixedGuillaume Boisseau2024-06-218-10/+19
|\
| * Update charonNadrieril2024-06-218-10/+19
|/
* Merge pull request #253 from Nadrieril/merge-preds-into-paramsGuillaume Boisseau2024-06-2110-77/+67
|\
| * `predicates` got merged into `generic_params`Nadrieril2024-06-2110-77/+67
|/
* Support for renaming using the rename attribute in charon (#239)Escherichia2024-06-1827-301/+2797
* Merge pull request #251 from Nadrieril/bump-charon2Guillaume Boisseau2024-06-1822-89/+73
|\
| * Revert "Switch to GitHub CI runners" againNadrieril2024-06-181-12/+4
| * 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
|\
| * 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
|\ \
| * \ 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
|/ / / /
| * | | 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 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
| | |\ \ | |_|/ / |/| | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 03:41:39 +0000