Disabled autoimplicits (for CI checks)

trishullab · Aug 17, 2024 · 9a9436d · 9a9436d
1 parent da40f2f
commit 9a9436d
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean
@@ -3,6 +3,9 @@ open Lake DSL
 
 package «putnam» where
   -- add package configuration options here
+  leanOptions := #[
+    ⟨`autoImplicit, false⟩
+  ]
 require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.10.0"
 
 @[default_target]