summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Vec.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-12Add more definitions to the Lean librarySon Ho1-0/+39
2024-04-05Update the lean toolchain and fix the proofsSon Ho1-1/+0
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho1-13/+13
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho1-1/+1
2024-02-02Fix more proofsSon Ho1-1/+1
2023-12-22Update the Lean standard librarySon Ho1-15/+23
2023-11-21Update the standard librariesSon Ho1-3/+3
2023-11-09Update the failing proofsSon Ho1-4/+22
2023-10-25Make the hashmap files typecheck again in LeanSon Ho1-29/+45
2023-10-25Fix some issues at extraction and add builtinsSon Ho1-1/+1
2023-09-18Prove that Vec is inhabitedSon Ho1-0/+4
2023-08-04Make minor modificationsSon Ho1-4/+4
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-11/+6
2023-07-26Update some of the Vec function specsSon Ho1-4/+9
2023-07-25Make progress on the proofs of the hashmapSon Ho1-12/+8
2023-07-25Make progress on the hashmap propertiesSon Ho1-3/+10
2023-07-25Improve int_tac and scalar_tacSon Ho1-13/+12
2023-07-18Make modifications to Vec.leanSon Ho1-3/+5
2023-07-17Start proving theorems for primitive definitionsSon Ho1-33/+56
2023-07-17Reorganize the Lean backendSon Ho1-0/+113
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 22:53:47 +0000