clean up lakefile.lean

m4lvin · Dec 9, 2024 · 532b71c · 532b71c
1 parent 43fe37c
commit 532b71c
Showing 1 changed file with 4 additions and 8 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -1,17 +1,13 @@
 import Lake
 open Lake DSL
 
-package «pdl» where
-  -- add any package configuration options here
+package «pdl»
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"@"v4.13.0"
 
--- require "marcusrossel" / "egg" @ git "main"
-
 @[default_target]
-lean_lib «Pdl» where
-  -- add any library configuration options here
+lean_lib «Pdl»
+
+lean_lib «Bml»
 
-lean_lib «Bml» where
-  -- add any library configuration options here