summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/Base.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-07-18Move an arithmetic lemmaSon Ho1-10/+4
2023-07-17Start proving theorems for primitive definitionsSon Ho1-2/+1
2023-07-12Improve progress to use assumptions and start working on a nice syntaxSon Ho1-22/+0
2023-07-12Finish a first version of the progress tacticSon Ho1-1/+1
2023-07-04Make Diverge use PrimitivesSon Ho1-64/+1
2023-07-04Add an implemented_by attribute to fixSon Ho1-11/+18
2023-07-03Generate the proofs of validity in Elab.leanSon Ho1-2/+74
2023-06-30Generate the fixed-point bodies in Elab.leanSon Ho1-4/+4
2023-06-29Write function to compute the input/output typesSon Ho1-1/+2
2023-06-29Generalize a bit FixI and add an exampleSon Ho1-109/+151
2023-06-29Start working on Elab.leanSon Ho1-0/+3
2023-06-28Reorganize backends/lean/BaseSon Ho1-2/+0
2023-06-27Reduce the time spent on some proofsSon Ho1-28/+20
2023-06-27Finish some proofs in DivergeSon Ho1-17/+102
2023-06-27Finish the proofs which use FixISon Ho1-42/+157
2023-06-26Make minor modificationsSon Ho1-16/+0
2023-06-26Add FixI in DivergeSon Ho1-22/+105
2023-06-26Generalize some definitionsSon Ho1-12/+22
2023-06-26Make the definitions in Diverge.Fix dependently typedSon Ho1-48/+47
2023-06-26Start working on a better encoding of mut rec defs for DivergeSon Ho1-2/+100
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 13:44:11 +0000