initial commit

lakefile.toml

@@ -0,0 +1,18 @@
+name = "colloquium-lean"
+version = "0.1.0"
+keywords = ["math"]
+defaultTargets = ["ColloquiumLean"]
+
+[leanOptions]
+pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+autoImplicit = false
+relaxedAutoImplicit = false
+weak.linter.mathlibStandardSet = true
+maxSynthPendingDepth = 3
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+
+[[lean_lib]]
+name = "ColloquiumLean"