summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Scalar.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO1-11/+0
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-3/+9
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-0/+2
2024-06-12Deactivate the coercion from Nat to ScalarSon Ho1-0/+10
2024-06-12Add the Simp.Config to the simp wrappersSon Ho1-24/+23
2024-05-24Update scalar_tac to use omega instead of linarithSon Ho1-1/+1
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho1-1/+1
2024-01-26Improve the Lean backendSon Ho1-2/+9
2023-10-17Refold the scalar types when applying progressSon Ho1-1/+1
2023-10-17Implement tactics for termination proofs which involve arithmeticSon Ho1-0/+11
2023-09-18Improve scalar_tacSon Ho1-2/+15
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-0/+4
2023-07-26Update the syntax of the progress tacticSon Ho1-1/+1
2023-07-25Make progress on the hashmap propertiesSon Ho1-1/+2
2023-07-25Improve int_tac and scalar_tacSon Ho1-3/+3
2023-07-17Reorganize the Lean backendSon Ho1-0/+48
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 13:08:03 +0000