summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Diverge/Base.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-7/+14
|
* Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-111-3/+1
|\
| * Update the lean toolchain and fix the proofsSon Ho2024-04-051-3/+1
| |
* | Rename Result.ret as Result.ok in the backendsSon Ho2024-04-041-51/+51
|/
* Update lean to v4.6.0-rc1 and start fixing the proofsSon Ho2024-02-021-15/+22
|
* Make progress on supporting higher-order divergent functionsSon Ho2023-12-121-10/+12
|
* Start working on higher-order examples for DivergeSon Ho2023-12-111-0/+3
|
* Update Diverge/Elab.lean to use the more general FixII definitionsSon Ho2023-12-111-7/+2
|
* Start working on a version of Diverge.FixI more suited to higher-order functionsSon Ho2023-12-071-67/+503
|
* Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-19/+16
|
* Move an arithmetic lemmaSon Ho2023-07-181-10/+4
|
* Start proving theorems for primitive definitionsSon Ho2023-07-171-2/+1
|
* Improve progress to use assumptions and start working on a nice syntaxSon Ho2023-07-121-22/+0
|
* Finish a first version of the progress tacticSon Ho2023-07-121-1/+1
|
* Make Diverge use PrimitivesSon Ho2023-07-041-64/+1
|
* Add an implemented_by attribute to fixSon Ho2023-07-041-11/+18
|
* Generate the proofs of validity in Elab.leanSon Ho2023-07-031-2/+74
|
* Generate the fixed-point bodies in Elab.leanSon Ho2023-06-301-4/+4
|
* Write function to compute the input/output typesSon Ho2023-06-291-1/+2
|
* Generalize a bit FixI and add an exampleSon Ho2023-06-291-109/+151
|
* Start working on Elab.leanSon Ho2023-06-291-0/+3
|
* Reorganize backends/lean/BaseSon Ho2023-06-281-0/+1105
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:55:45 +0000