aboutsummaryrefslogtreecommitdiff
path: root/lakefile.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2024-07-22 00:18:36 +0200
committerAndreas Grois <andi@grois.info>2024-07-22 00:18:36 +0200
commit1ff5b4e46f52fa05624523b17a5188991ab82cf3 (patch)
treea487ff5b7ec7db0d3578d3077e3d29c6c68e00a0 /lakefile.lean
Initial commit.
Diffstat (limited to 'lakefile.lean')
-rw-r--r--lakefile.lean7
1 files changed, 7 insertions, 0 deletions
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..c1a725e
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package «BinaryHeap» where
+
+@[default_target]
+lean_lib «BinaryHeap» where