summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Array.lean (follow)
Commit message (Expand)AuthorAgeFilesLines
* Fix issues with the extraction and extend the primitive libraries for Coq and F*Son Ho2023-08-041-14/+14
* Add SliceLen as a primitive function and make minor adjustmentsSon Ho2023-08-041-42/+38
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-041-0/+398