summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Arith.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-07-17Reorganize the Lean backendSon Ho1-329/+0
2023-07-17Move a definitionSon Ho1-3/+0
2023-07-13Update a commentSon Ho1-2/+1
2023-07-13Add IList.leanSon Ho1-64/+72
2023-07-12Improve progress to use assumptions and start working on a nice syntaxSon Ho1-41/+1
2023-07-12Improve the handling of arithmetic boundsSon Ho1-2/+6
2023-07-12Finish a first version of the progress tacticSon Ho1-93/+29
2023-07-11Work on the progress tacticSon Ho1-13/+29
2023-07-10Start working on the progress tacticSon Ho1-58/+3
2023-07-09Improve int_tacSon Ho1-23/+18
2023-07-09Implement a first working version of int_tacSon Ho1-38/+58
2023-07-09Make progress on the int tacticSon Ho1-156/+257
2023-06-26Make minor modifications to Arith.leanSon Ho1-27/+37
2023-06-22Make intro_has_prop_instances workSon Ho1-26/+145
2023-06-22Finish the custom_let tacticSon Ho1-23/+21
2023-06-21Start working on Arith.leanSon Ho1-0/+221