summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Vec.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-0/+4
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO1-5/+2
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-2/+11
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-2/+1
2024-06-13Fix more issuesSon Ho1-2/+2
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-23 10:41:05 +0000