summaryrefslogtreecommitdiff
path: root/backends/lean/Base/IList/IList.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Do some cleanup in the Lean backend (#257)Son HO2024-06-221-9/+9
* Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2024-06-221-20/+41
* Add some proofs for the Lean backend (#255)Son HO2024-06-211-2/+21
* Merge branch 'son/update-lean' into has-int-predSon Ho2024-06-171-6/+6
|\
| * Update Lean to v4.9.0-rc1Son Ho2024-06-131-6/+6
* | backends/lean: introduce `HasIntPred` automationRyan Lahfa2024-06-121-3/+5
|/
* Fix tuple indexing for Lean backendZyad Hassan2024-03-081-1/+1
* Fix more proofsSon Ho2024-02-021-11/+14
* Merge branch 'main' into son_fixes2Son Ho2023-12-051-1/+38
|\
| * Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-171-21/+3
| * Merge branch 'main' into son_traits and fix some issuesSon Ho2023-10-161-3/+2
| |\
| * | Add supSon Ho2023-10-131-1/+56
* | | Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho2023-09-181-9/+7
| |/ |/|
* | Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-3/+2
|/
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-041-9/+229
* Make progress on the proofs of the hashmapSon Ho2023-07-251-0/+41
* Improve int_tac and scalar_tacSon Ho2023-07-251-8/+4
* Improve progress further and move some lemmasSon Ho2023-07-201-0/+67
* Start proving theorems for primitive definitionsSon Ho2023-07-171-14/+52
* Reorganize the Lean backendSon Ho2023-07-171-0/+142
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 15:26:23 +0000