summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/ElabBase.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update lean to v4.6.0-rc1 and start fixing the proofsSon Ho2024-02-021-6/+10
|
* Start working on higher-order examples for DivergeSon Ho2023-12-111-1/+62
|
* Update Diverge/Elab.lean to use the more general FixII definitionsSon Ho2023-12-111-0/+2
|
* 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