summaryrefslogtreecommitdiff
path: root/backends/lean/Base/IList (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-9/+9
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO1-20/+41
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-2/+21
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-6/+6
2024-06-12backends/lean: introduce `HasIntPred` automationRyan Lahfa1-3/+5
2024-03-08Fix tuple indexing for Lean backendZyad Hassan1-1/+1
2024-02-02Fix more proofsSon Ho1-11/+14
2023-10-17Implement tactics for termination proofs which involve arithmeticSon Ho1-21/+3
2023-10-13Add supSon Ho1-1/+56
2023-09-18Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho1-9/+7
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho1-3/+2
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-9/+229
2023-07-25Make progress on the proofs of the hashmapSon Ho1-0/+41
2023-07-25Improve int_tac and scalar_tacSon Ho1-8/+4
2023-07-20Improve progress further and move some lemmasSon Ho1-0/+67
2023-07-17Start proving theorems for primitive definitionsSon Ho1-14/+52
2023-07-17Reorganize the Lean backendSon Ho1-0/+142
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 03:21:55 +0000