summaryrefslogtreecommitdiff
path: root/tests/lean/lakefile.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-08-03Fix issuesSon Ho1-0/+1
2023-07-05Start using namespaces in the Lean backendSon Ho1-12/+9
2023-07-04Regenerate the Lean test filesSon Ho1-0/+8
2023-07-04Reorganize the Lean testsSon Ho1-3/+5
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