Enable experimental module system yay

Changes

1 changed files (+1/-1)

• lakefile.toml
  • @@ -6,9 +6,9 @@ defaultTargets = ["miscelleaneous"]
    pp.unicode.fun = true # pretty-prints `fun a ↦ b` relaxedAutoImplicit = false weak.linter.mathlibStandardSet = true - weak.linter.flexible = true weak.linter.style.longLine = false maxSynthPendingDepth = 3 + experimental.module = true [[lean_exe]] name = "miscelleaneous"