summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/Elab.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-05Update the lean toolchain and fix the proofsSon Ho1-1/+0
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 Ho1-7/+4
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 Ho1-43/+83
2023-12-11Update the validity proofs for higher-order functionsSon Ho1-8/+93
2023-12-11Start working on higher-order examples for DivergeSon Ho1-213/+288
2023-12-11Cleanup a bitSon Ho1-16/+47
2023-12-11Update Diverge/Elab.lean to use the more general FixII definitionsSon Ho1-188/+383
2023-12-07Reorganize a bitSon Ho1-4/+20
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho1-1/+1
2023-07-10Start working on the progress tacticSon Ho1-16/+1
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 Ho1-85/+143
2023-07-04Fix some issues with the extraction to LeanSon Ho1-16/+47
2023-07-04Make Diverge use PrimitivesSon Ho1-1/+1
2023-07-03Cleanup a bit Diverge/Elab.leanSon Ho1-169/+197
2023-07-03Automate the proofs of the unfolding theorems for DivergeSon Ho1-19/+88
2023-07-03Add a missing case in the validity proofsSon Ho1-6/+19
2023-07-03Generate the proofs of validity in Elab.leanSon Ho1-32/+371
2023-06-30Generate the fixed-point bodies in Elab.leanSon Ho1-107/+344
2023-06-29Write function to compute the input/output typesSon Ho1-31/+123
2023-06-29Start working on Elab.leanSon Ho1-11/+127
2023-06-28Reorganize backends/lean/BaseSon Ho1-0/+182
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 16:47:32 +0000