summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives (unfollow)
Commit message (Expand)AuthorFilesLines
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-04Start adding support for Arrays/Slices in the Lean librarySon Ho4-20/+425
2023-07-26Update some of the Vec function specsSon Ho1-4/+9
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+43
2023-07-25Make progress on the proofs of the hashmapSon Ho2-13/+9
2023-07-25Make progress on the hashmap propertiesSon Ho2-24/+37
2023-07-25Improve int_tac and scalar_tacSon Ho1-13/+12
2023-07-20Add fine-grained lemmas for the arithmetic operationsSon Ho1-7/+130
2023-07-19Add arithmetic spec lemmasSon Ho1-6/+161
2023-07-18Make modifications to Vec.leanSon Ho1-3/+5
2023-07-17Start proving theorems for primitive definitionsSon Ho2-33/+57
2023-07-17Reorganize the Lean backendSon Ho3-0/+750