summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ArraySlice.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-04-12Reorganize the files in the Lean backend a bitSon Ho1-1/+1
2024-04-05Update the lean toolchain and fix the proofsSon Ho1-3/+2
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho1-27/+27
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho1-1/+1
2024-02-02Fix more proofsSon Ho1-1/+1
2023-12-22Fix minor issuesSon Ho1-0/+42
2023-12-22Update the Lean standard librarySon Ho1-57/+11
2023-11-21Update more namesSon Ho1-16/+16
2023-11-21Update the standard librariesSon Ho1-20/+19
2023-10-26Make progress on fixing the extractionSon Ho1-64/+64
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-114/+50
2023-10-25Make the hashmap files typecheck again in LeanSon Ho1-2/+59
2023-10-25Fix some issues at extraction and add builtinsSon Ho1-1/+158
2023-10-13Add supSon Ho1-0/+9
2023-08-04Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho1-14/+14
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 Ho1-0/+398
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 07:57:14 +0000