summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ArraySlice.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-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