Migrate to a lakefile.toml.

leanprover-community · Aug 1, 2024 · 9567b65 · 9567b65
1 parent 1d621d5
commit 9567b65
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 20 deletions.
diff --git a/lakefile.lean b/lakefile.lean
diff --git a/lakefile.toml b/lakefile.toml
@@ -0,0 +1,18 @@
+name = "SphereEversion"
+defaultTargets = ["SphereEversion"]
+
+[leanOptions]
+pp.unicode.fun = true
+autoImplicit = false
+relaxedAutoImplicit = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+
+[[require]]
+name = "checkdecls"
+git = "https://github.com/PatrickMassot/checkdecls.git"
+
+[[lean_lib]]
+name = "SphereEversion"