summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge (unfollow)
Commit message (Expand)AuthorFilesLines
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