summaryrefslogtreecommitdiff
path: root/tests/lean/misc/external/lakefile.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Generate all the lakefile.lean filesSon Ho1-2/+2
2023-06-04Automate the generation of the lakefile.lean filesSon Ho1-7/+3
2023-06-04Fill out Primitives.leanJonathan Protzenko1-0/+3
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko1-1/+5
2023-06-04Add a sample test to illustrate potential project structureJonathan Protzenko1-0/+15