From 51f01d8c8a25cc8ec7bcd4db1e618031a06dc972 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 19 Aug 2024 09:57:16 +0200
Subject: [PATCH] feat: expose `index` option to `dsimp` tactic (#5071)

makes the option introduced in #4202 also available when using `dsimp`
---
 src/Init/MetaTypes.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index 1f0b52cc6e..06e8f37f74 100644
--- 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