fix: withInferTypeConfig

leanprover · Nov 29, 2024 · a46cb57 · a46cb57
1 parent c5fcab1
commit a46cb57
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
@@ -187,7 +187,7 @@ because it overrides unrelated configurations.
 @[inline] def withInferTypeConfig (x : MetaM α) : MetaM α :=
   withAtLeastTransparency .default do
     let cfg ← getConfig
-    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj != .no then
+    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then
       x
     else
       withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x