iota := true is the default, so it can be removed

leanprover · Feb 4, 2025 · e13dde2 · e13dde2
1 parent fef8b6a
commit e13dde2
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -197,8 +197,7 @@ structure SimpTheorems where
 Configuration for `MetaM` used to process global simp theorems
 -/
 def simpGlobalConfig : ConfigWithKey :=
-  { iota         := true
-    proj         := .no
+  { proj         := .no
     zetaDelta    := false
     transparency := .reducible
   : Config }.toConfigWithKey