feat: add Simp.Config.implicitDefEqProofs

This commit does **not** implement this feature.

Author: leodemoura

src/Init/MetaTypes.lean

@@ -218,6 +218,14 @@ structure Config where
   to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
   -/
   index             : Bool := true
+  /--
+  When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated
+  with an `rfl`-theorem.
+  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
+  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
+  will **not** create a proof term which is an application of the annotated theorem.
+  -/
+  implicitDefEqProofs : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`