summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Improve int_tacSon Ho2023-07-091-23/+18
* Implement a first working version of int_tacSon Ho2023-07-091-38/+58
* Make progress on the int tacticSon Ho2023-07-091-156/+257
* Make minor modifications to Arith.leanSon Ho2023-06-261-27/+37
* Make intro_has_prop_instances workSon Ho2023-06-221-26/+145
* Finish the custom_let tacticSon Ho2023-06-221-23/+21
* Start working on Arith.leanSon Ho2023-06-211-0/+221