summaryrefslogtreecommitdiff
path: root/backends/lean/Base/IList (follow)
Commit message (Expand)AuthorAgeFilesLines
* 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
|\
| * Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-3/+2
* | Add supSon Ho2023-10-131-1/+56
|/
* 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