summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Base.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Add some proofs for the Lean backend (#255)Son HO2024-06-211-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-6/+5
|
* Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-171-0/+12
|
* Make progress on the hashmap propertiesSon Ho2023-07-251-0/+4
|
* Move an arithmetic lemmaSon Ho2023-07-181-0/+6
|
* Add IList.leanSon Ho2023-07-131-0/+40
|
* Start working on the progress tacticSon Ho2023-07-101-0/+10
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 13:27:59 +0000