summaryrefslogtreecommitdiff
path: root/backends/lean/Base/IList/IList.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-6/+6
* 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-12-23 12:56:12 +0000