summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Array.lean (unfollow)
Commit message (Expand)AuthorFilesLines
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