summaryrefslogtreecommitdiff
path: root/tests/lean/misc-constants/lakefile.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Update the extraction of Lean filesSon Ho1-10/+4
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho1-0/+0
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