summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Int.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Refold the scalar types when applying progressSon Ho2023-10-171-2/+2
* Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-171-0/+11
* Improve scalar_tacSon Ho2023-09-181-3/+5
* 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-041-10/+21
* Update the syntax of the progress tacticSon Ho2023-07-261-1/+1
* Make progress on the proofs of the hashmapSon Ho2023-07-251-0/+1
* Make progress on the hashmap propertiesSon Ho2023-07-251-0/+2
* Improve int_tac and scalar_tacSon Ho2023-07-251-7/+56
* Make some proofs in Hashmap/Properties.lean and improve progressSon Ho2023-07-201-1/+1
* Improve progressSon Ho2023-07-191-8/+0
* Reorganize the Lean backendSon Ho2023-07-171-0/+236