summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-05Update the lean toolchain and fix the proofsSon Ho2-4/+1
2024-03-09Fix an issue with the divergent encodingSon Ho1-3/+27
2024-02-02Update lean to v4.6.0-rc1 and start fixing the proofsSon Ho3-28/+36
2023-12-12Inline the let-bindings in the validity proofsSon Ho1-7/+40
2023-12-12Fix a minor issue with the divergent encodingSon Ho1-53/+80
2023-12-12Fix minor issues with the divergence encodingSon Ho1-14/+5
2023-12-12Make progress on supporting higher-order divergent functionsSon Ho2-53/+95
2023-12-11Update the validity proofs for higher-order functionsSon Ho1-8/+93
2023-12-11Start working on higher-order examples for DivergeSon Ho3-214/+353
2023-12-11Cleanup a bitSon Ho1-16/+47
2023-12-11Update Diverge/Elab.lean to use the more general FixII definitionsSon Ho3-195/+387
2023-12-07Start working on a version of Diverge.FixI more suited to higher-order functionsSon Ho2-67/+509
2023-12-07Reorganize a bitSon Ho1-4/+20
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho2-20/+17
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-10Start working on the progress tacticSon Ho1-16/+1
2023-07-09Make progress on the int tacticSon Ho1-112/+0
2023-07-06Reorganize a bit the lean backend filesSon Ho1-0/+2
2023-07-06Register the unfolding theorems in the Lean equation compilers and solve a "u...Son Ho1-2/+12
2023-07-04Fix an issue with mkSigmasValSon Ho2-106/+169
2023-07-04Fix some issues with the extraction to LeanSon Ho1-16/+47
2023-07-04Make Diverge use PrimitivesSon Ho3-69/+6
2023-07-04Add an implemented_by attribute to fixSon Ho1-11/+18
2023-07-03Cleanup a bit Diverge/Elab.leanSon Ho1-169/+197
2023-07-03Automate the proofs of the unfolding theorems for DivergeSon Ho2-19/+89
2023-07-03Add a missing case in the validity proofsSon Ho1-6/+19
2023-07-03Generate the proofs of validity in Elab.leanSon Ho3-34/+446
2023-06-30Generate the fixed-point bodies in Elab.leanSon Ho3-115/+391
2023-06-29Write function to compute the input/output typesSon Ho3-32/+126
2023-06-29Generalize a bit FixI and add an exampleSon Ho1-109/+151
2023-06-29Start working on Elab.leanSon Ho3-13/+203
2023-06-28Reorganize backends/lean/BaseSon Ho3-0/+1296
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:13:43 +0000