summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Int.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO1-6/+13
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-7/+41
2024-06-17Make a minor cleanupSon Ho1-9/+11
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-4/+4
2024-06-12Add the Simp.Config to the simp wrappersSon Ho1-3/+3
2024-06-12backends/lean: introduce `HasIntPred` automationRyan Lahfa1-5/+33
2024-06-11feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa1-1/+1
2024-05-24Update scalar_tac to use omega instead of linarithSon Ho1-97/+65
2024-04-05Update the lean toolchain and fix the proofsSon Ho1-1/+0
2023-10-17Refold the scalar types when applying progressSon Ho1-2/+2
2023-10-17Implement tactics for termination proofs which involve arithmeticSon Ho1-0/+11
2023-09-18Improve scalar_tacSon Ho1-3/+5
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho1-1/+1
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-10/+21
2023-07-26Update the syntax of the progress tacticSon Ho1-1/+1
2023-07-25Make progress on the proofs of the hashmapSon Ho1-0/+1
2023-07-25Make progress on the hashmap propertiesSon Ho1-0/+2
2023-07-25Improve int_tac and scalar_tacSon Ho1-7/+56
2023-07-20Make some proofs in Hashmap/Properties.lean and improve progressSon Ho1-1/+1
2023-07-19Improve progressSon Ho1-8/+0
2023-07-17Reorganize the Lean backendSon Ho1-110/+17
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 11:26:54 +0000