summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/ElabBase.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Start working on a version of Diverge.FixI more suited to higher-order functionsSon Ho2023-12-071-0/+6
* Make progress on the int tacticSon Ho2023-07-091-112/+0
* Fix an issue with mkSigmasValSon Ho2023-07-041-21/+26
* 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