summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Scalar.lean (unfollow)
Commit message (Expand)AuthorFilesLines
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