summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ArraySlice.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-0/+8
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-1/+1
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-2/+1
2024-06-13Fix a proofSon Ho1-1/+1
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-23 08:28:07 +0000