diff options
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 |