feat: change (d)simp's default zeta value to false

As requested to test in leanprover#2682.
ericrbg · Oct 27, 2023 · ab8fdef · ab8fdef
1 parent f76a17b
commit ab8fdef
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
@@ -1219,7 +1219,7 @@ inductive EtaStructMode where
 namespace DSimp
 
 structure Config where
-  zeta              : Bool := true
+  zeta              : Bool := false
   beta              : Bool := true
   eta               : Bool := true
   etaStruct         : EtaStructMode := .all
@@ -1244,7 +1244,7 @@ structure Config where
   contextual        : Bool := false
   memoize           : Bool := true
   singlePass        : Bool := false
-  zeta              : Bool := true
+  zeta              : Bool := false
   beta              : Bool := true
   eta               : Bool := true
   etaStruct         : EtaStructMode := .all