summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/ElabBase.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Make Diverge use PrimitivesSon Ho2023-07-041-4/+4
* Automate the proofs of the unfolding theorems for DivergeSon Ho2023-07-031-0/+1
* Generate the proofs of validity in Elab.leanSon Ho2023-07-031-0/+1
* Generate the fixed-point bodies in Elab.leanSon Ho2023-06-301-4/+43
* Write function to compute the input/output typesSon Ho2023-06-291-0/+1
* Start working on Elab.leanSon Ho2023-06-291-2/+73
* Reorganize backends/lean/BaseSon Ho2023-06-281-0/+9