summaryrefslogtreecommitdiff
path: root/backends/lean/Base (follow)
Commit message (Expand)AuthorAgeFilesLines
* Finish the custom_let tacticSon Ho2023-06-221-23/+21
* Start working on Arith.leanSon Ho2023-06-212-2/+223
* Remove the use of fun. ext. in Diverge.leanSon Ho2023-06-201-15/+19
* Cleanup Diverge.leanSon Ho2023-06-192-337/+333
* Add an example with even/odd in Diverge.leanSon Ho2023-06-191-1/+119
* Remove the obsolete examples from DivergeSon Ho2023-06-191-208/+5
* Simplify the id example in Diverge.leanSon Ho2023-06-191-24/+95
* Further simplify the proofs in Diverge.leanSon Ho2023-06-191-122/+151
* Make progress on making the proofs in Diverge more systematicSon Ho2023-06-191-8/+252
* Make minor modificationsSon Ho2023-06-181-3/+2
* Make minor modificationsSon Ho2023-06-142-6/+26
* Find sufficient validity criteria for Diverge.leanSon Ho2023-06-131-41/+309
* Start working on extrinsic proofs of terminationSon Ho2023-06-092-7/+230
* Reorganize a bit the Lean librarySon Ho2023-06-091-0/+650