chore: remove unneeded experimental.module option

kim-em · kim-em · commit 32ca50ba6f72 · 2025-12-16T10:23:41.000+11:00
diff --git a/lakefile.toml b/lakefile.toml
@@ -2,9 +2,6 @@ name = "Qq"
 testDriver = "QqTest"
 defaultTargets = ["Qq"]
 
-[leanOptions]
-experimental.module = true
-
 [[lean_lib]]
 name = "Qq"
 
