summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-21Start working on Arith.leanSon Ho1-2/+2
2023-06-20Remove the use of fun. ext. in Diverge.leanSon Ho1-15/+19
2023-06-19Cleanup Diverge.leanSon Ho1-337/+320
2023-06-19Add an example with even/odd in Diverge.leanSon Ho1-1/+119
2023-06-19Remove the obsolete examples from DivergeSon Ho1-208/+5
2023-06-19Simplify the id example in Diverge.leanSon Ho1-24/+95
2023-06-19Further simplify the proofs in Diverge.leanSon Ho1-122/+151
2023-06-19Make progress on making the proofs in Diverge more systematicSon Ho1-8/+252
2023-06-14Make minor modificationsSon Ho1-6/+25
2023-06-13Find sufficient validity criteria for Diverge.leanSon Ho1-41/+309
2023-06-09Start working on extrinsic proofs of terminationSon Ho1-0/+208