From 98eb18bc338c7292d58404f81b86cbc0fcc11c51 Mon Sep 17 00:00:00 2001 From: tzlil Date: Fri, 15 Mar 2024 17:20:40 +0200 Subject: cool stuff --- lakefile.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 lakefile.lean (limited to 'lakefile.lean') 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 -- cgit 1.4.1