summaryrefslogtreecommitdiff
path: root/backends/lean/lakefile.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-09Reorganize a bit the Lean librarySon Ho1-1/+1
2023-06-06Remove the sorries from Primitives.leanSon Ho1-0/+1
2023-06-04Add backends/lean/lakefile.leanSon Ho1-4/+2
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