feat: expose index option to dsimp tactic (#5071)

makes the option introduced in #4202 also available when using `dsimp`
leanprover · Aug 19, 2024 · 51f01d8 · 51f01d8
1 parent b486c67
commit 51f01d8
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
@@ -104,6 +104,11 @@ structure Config where
   That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
   -/
   zetaDelta         : Bool := false
+  /--
+  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
+  to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
+  -/
+  index             : Bool := true
   deriving Inhabited, BEq
 
 end DSimp