summaryrefslogtreecommitdiff
path: root/backends/lean (unfollow)
Commit message (Expand)AuthorFilesLines
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
2023-06-20Remove the use of fun. ext. in Diverge.leanSon Ho1-15/+19
2023-06-19Cleanup Diverge.leanSon Ho2-337/+333
2023-06-19Add an example with even/odd in Diverge.leanSon Ho1-1/+119
2023-06-19Remove the obsolete examples from DivergeSon Ho1-208/+5
2023-06-19Simplify the id example in Diverge.leanSon Ho1-24/+95
2023-06-19Further simplify the proofs in Diverge.leanSon Ho1-122/+151
2023-06-19Make progress on making the proofs in Diverge more systematicSon Ho1-8/+252
2023-06-18Make minor modificationsSon Ho2-3/+3
2023-06-14Make minor modificationsSon Ho2-6/+26
2023-06-13Find sufficient validity criteria for Diverge.leanSon Ho1-41/+309
2023-06-09Start working on extrinsic proofs of terminationSon Ho4-7/+232
2023-06-09Reorganize a bit the Lean librarySon Ho4-22/+36
2023-06-06Remove the sorries from Primitives.leanSon Ho2-65/+120
2023-06-04Add Result_Inhabited to Primitives.leanSon Ho1-0/+3
2023-06-04Make more updates for the Lean backendSon Ho1-33/+57
2023-06-04Update Primitives.leanSon Ho1-90/+58
2023-06-04Update Primitives.leanSon Ho1-194/+390
2023-06-04Add backends/lean/lakefile.leanSon Ho3-0/+39
2023-06-04Make minor modifications and regenerate the Lean filesSon Ho1-1/+1
2023-06-04WIPJonathan Protzenko1-35/+41
2023-06-04More commentsJonathan Protzenko1-40/+53
2023-06-04Idiomatic naming conventionsJonathan Protzenko1-46/+46
2023-06-04Rename primitives.lean to Primitives.leanSon Ho1-0/+0
2023-06-04WIPJonathan Protzenko1-26/+50
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko1-2/+26
2023-06-04Remove last sorry in PrimitivesJonathan Protzenko1-10/+105
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko1-3/+30
2023-06-04WIP lots of stuffJonathan Protzenko1-5/+30
2023-06-04Fixup one primitive that is not assumed to be monadicJonathan Protzenko1-4/+4
2023-06-04More cosmetic improvementsJonathan Protzenko1-0/+1
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-01 06:34:27 +0000