summaryrefslogtreecommitdiff
path: root/backends/lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-09-18Prove that Vec is inhabitedSon Ho1-0/+4
2023-09-18Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho2-9/+10
2023-09-18Add notations for the Isize.ofInt, etc.Son Ho1-0/+16
2023-09-18Add arithmetic lemmas in Scalar.leanSon Ho1-12/+179
2023-09-18Improve scalar_tacSon Ho3-56/+36
2023-09-18Fix an issue when loading the saved theorem maps for the progress tacticSon Ho2-3/+68
2023-09-14Fix the hashmap proofs in LeanSon Ho2-7/+8
2023-09-14Fix panic issues with the progress tacticSon Ho1-3/+5
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho7-38/+50
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho1-14/+14
2023-08-04Make minor modificationsSon Ho1-4/+4
2023-08-04Add SliceLen as a primitive function and make minor adjustmentsSon Ho1-42/+38
2023-08-04Add the UtilsBase.lean fileSon Ho1-0/+10
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho8-39/+680
2023-07-26Update some of the Vec function specsSon Ho2-9/+21
2023-07-26Update the syntax of the progress tacticSon Ho4-25/+32
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+43
2023-07-25Make progress on the proofs of the hashmapSon Ho6-30/+104
2023-07-25Make progress on the hashmap propertiesSon Ho7-29/+49
2023-07-25Improve int_tac and scalar_tacSon Ho5-32/+87
2023-07-25Add the possibility of using "_" as ident for progressSon Ho2-18/+26
2023-07-25Improve the syntax of progress: `as ⟨ x, y .. ⟩`Son Ho2-44/+94
2023-07-20Fix a naming issue with progressSon Ho1-4/+4
2023-07-20Make progress on some of the hashmap proofsSon Ho1-8/+22
2023-07-20Make some proofs in Hashmap/Properties.lean and improve progressSon Ho4-63/+64
2023-07-20Improve progress further and move some lemmasSon Ho2-21/+101
2023-07-20Add fine-grained lemmas for the arithmetic operationsSon Ho2-8/+131
2023-07-20Improve progress furtherSon Ho2-72/+142
2023-07-19Fix a small issue with the persistent state of progressSon Ho2-5/+13
2023-07-19Add some utilities for progressSon Ho2-5/+35
2023-07-19Add arithmetic spec lemmasSon Ho1-6/+161
2023-07-19Start implementing support for some type classes for progressSon Ho2-25/+117
2023-07-19Cleanup moreSon Ho1-3/+0
2023-07-19Cleanup a bitSon Ho1-2/+0
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 Ho3-64/+239
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 19:58:34 +0000