chore: enable three hopefully-innocuous linters

leanprover-community · Nov 20, 2024 · 8d9e86e · 8d9e86e
1 parent 5dfbaac
commit 8d9e86e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/lakefile.toml b/lakefile.toml
@@ -5,6 +5,9 @@ defaultTargets = ["SphereEversion"]
 pp.unicode.fun = true
 autoImplicit = false
 relaxedAutoImplicit = false
+linter.oldObtain = true
+linter.refine = true
+linter.style.multiGoal = true
 
 [[require]]
 name = "mathlib"