summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Scalar.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2024-06-221-11/+0
* Add some proofs for the Lean backend (#255)Son HO2024-06-211-3/+9
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-0/+2
* Deactivate the coercion from Nat to ScalarSon Ho2024-06-121-0/+10
* Add the Simp.Config to the simp wrappersSon Ho2024-06-121-24/+23
* Update scalar_tac to use omega instead of linarithSon Ho2024-05-241-1/+1
* 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-171-1/+1
* Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-171-0/+11
* Improve scalar_tacSon Ho2023-09-181-2/+15
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-041-0/+4
* Update the syntax of the progress tacticSon Ho2023-07-261-1/+1
* Make progress on the hashmap propertiesSon Ho2023-07-251-1/+2
* Improve int_tac and scalar_tacSon Ho2023-07-251-3/+3
* Reorganize the Lean backendSon Ho2023-07-171-0/+48
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 15:26:12 +0000