summaryrefslogtreecommitdiff
path: root/backends (unfollow)
Commit message (Expand)AuthorFilesLines
2023-07-19Improve progressSon Ho3-43/+99
2023-07-18Move an arithmetic lemmaSon Ho2-10/+10
2023-07-18Make modifications to Vec.leanSon Ho1-3/+5
2023-07-18Improve progressSon Ho3-5/+21
2023-07-17Start proving theorems for primitive definitionsSon Ho6-50/+116
2023-07-17Reorganize the Lean backendSon Ho11-1171/+1184
2023-07-17Move a definitionSon Ho2-3/+3
2023-07-17Update the lean dependencies and update IListSon Ho5-9/+12
2023-07-13Update a commentSon Ho1-2/+1
2023-07-13Add IList.leanSon Ho4-64/+242
2023-07-13Finish implementing the syntax for `progress`Son Ho2-38/+107
2023-07-12Improve progress to use assumptions and start working on a nice syntaxSon Ho5-95/+140
2023-07-12Make the `by inlit` implicitSon Ho1-8/+7
2023-07-12Improve the handling of arithmetic boundsSon Ho3-115/+126
2023-07-12Finish a first version of the progress tacticSon Ho6-171/+349
2023-07-11Work on the progress tacticSon Ho6-13/+346
2023-07-10Start working on the progress tacticSon Ho5-74/+101
2023-07-09Improve int_tacSon Ho1-23/+18
2023-07-09Implement a first working version of int_tacSon Ho1-38/+58
2023-07-09Make progress on the int tacticSon Ho3-268/+267
2023-07-06Reorganize a bit the lean backend filesSon Ho2-0/+121
2023-07-06Register the unfolding theorems in the Lean equation compilers and solve a "u...Son Ho1-2/+12
2023-07-06Improve the generated commentsSon Ho1-1/+1
2023-07-05Simplify the names used in Primitives.leanSon Ho1-16/+21
2023-07-04Fix an issue with mkSigmasValSon Ho3-107/+170
2023-07-04Fix some issues with the extraction to LeanSon Ho1-16/+47
2023-07-04Reorganize the Lean testsSon Ho3-4/+9
2023-07-04Make Diverge use PrimitivesSon Ho4-90/+10
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 Ho4-1102/+1298
2023-06-27Reduce the time spent on some proofsSon Ho1-28/+20
2023-06-27Finish some proofs in DivergeSon Ho1-17/+102
2023-06-27Finish the proofs which use FixISon Ho1-42/+157
2023-06-26Make minor modificationsSon Ho1-16/+0
2023-06-26Add FixI in DivergeSon Ho1-22/+105
2023-06-26Generalize some definitionsSon Ho1-12/+22
2023-06-26Make the definitions in Diverge.Fix dependently typedSon Ho1-48/+47
2023-06-26Start working on a better encoding of mut rec defs for DivergeSon Ho1-2/+100
2023-06-26Make minor modifications to Arith.leanSon Ho1-27/+37
2023-06-22Make intro_has_prop_instances workSon Ho1-26/+145
2023-06-22Finish the custom_let tacticSon Ho1-23/+21
2023-06-21Start working on Arith.leanSon Ho3-2/+224
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 08:48:56 +0000