Add backends/lean/lakefile.lean

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» {}