summaryrefslogtreecommitdiff
path: root/backends/lean/lakefile.lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/lakefile.lean')
-rw-r--r--backends/lean/lakefile.lean10
1 files changed, 10 insertions, 0 deletions
diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
new file mode 100644
index 00000000..9633e1e8
--- /dev/null
+++ b/backends/lean/lakefile.lean
@@ -0,0 +1,10 @@
+import Lake
+open Lake DSL
+
+require mathlib from git
+ "https://github.com/leanprover-community/mathlib4.git"
+
+package «base» {}
+
+@[default_target]
+lean_lib «Primitives» {}