Make leanOptions match default math lakefile.toml template, except autoImplicit is nice so I'll keep that enabled

Changes

1 changed files (+7/-4)

• lakefile.toml
  • @@ -2,10 +2,13 @@ name = "miscelleaneous"
    version = "0.1.0" defaultTargets = ["miscelleaneous"] - [leanOptions.weak.linter] - mathlibStandardSet = true - flexible = true - style.longLine = false + [leanOptions] + 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 [[lean_exe]] name = "miscelleaneous"