summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/Elab.lean (unfollow)
Commit message (Expand)AuthorFilesLines
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-25 19:53:31 +0000