diff options
author | tzlil <tzlils@protonmail.com> | 2024-03-15 17:20:40 +0200 |
---|---|---|
committer | tzlil <tzlils@protonmail.com> | 2024-03-15 17:20:40 +0200 |
commit | 98eb18bc338c7292d58404f81b86cbc0fcc11c51 (patch) | |
tree | 6c18fbc674dbc9950e886e7aaea09f8bb5ce748c /lakefile.lean |
cool stuff
Diffstat (limited to 'lakefile.lean')
-rw-r--r-- | lakefile.lean | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..a961071 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,16 @@ +import Lake +open Lake DSL + +package «bananas» where + -- add package configuration options here + +lean_lib «Bananas» where + -- add library configuration options here + +@[default_target] +lean_exe «bananas» where + root := `Main + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true |