summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Vec.lean (unfollow)
Commit message (Expand)AuthorFilesLines
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 23:10:25 +0000