summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith (follow)
Commit message (Expand)AuthorAgeFilesLines
* Deactivate the coercion from Nat to ScalarSon Ho2024-06-121-0/+10
* Add the Simp.Config to the simp wrappersSon Ho2024-06-122-27/+26
* Update scalar_tac to use omega instead of linarithSon Ho2024-05-243-98/+66
* Update the lean toolchain and fix the proofsSon Ho2024-04-051-1/+0
* Update the handling of notations like #u32 or #isizeSon Ho2024-03-081-1/+1
* Improve the Lean backendSon Ho2024-01-261-2/+9
* Refold the scalar types when applying progressSon Ho2023-10-172-3/+3
* Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-173-0/+34
* Improve scalar_tacSon Ho2023-09-182-5/+20
* Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-1/+1
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-042-10/+25
* Update the syntax of the progress tacticSon Ho2023-07-262-2/+2
* Make progress on the proofs of the hashmapSon Ho2023-07-251-0/+1
* Make progress on the hashmap propertiesSon Ho2023-07-253-1/+8
* Improve int_tac and scalar_tacSon Ho2023-07-252-10/+59
* Make some proofs in Hashmap/Properties.lean and improve progressSon Ho2023-07-201-1/+1
* Improve progressSon Ho2023-07-191-8/+0
* Move an arithmetic lemmaSon Ho2023-07-181-0/+6
* Reorganize the Lean backendSon Ho2023-07-173-329/+284
* Move a definitionSon Ho2023-07-171-3/+0
* Update a commentSon Ho2023-07-131-2/+1
* Add IList.leanSon Ho2023-07-132-64/+112
* Improve progress to use assumptions and start working on a nice syntaxSon Ho2023-07-121-41/+1
* Improve the handling of arithmetic boundsSon Ho2023-07-121-2/+6
* Finish a first version of the progress tacticSon Ho2023-07-121-93/+29
* Work on the progress tacticSon Ho2023-07-111-13/+29
* Start working on the progress tacticSon Ho2023-07-102-0/+419
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:30:03 +0000