chore: add iff_self to simpOnlyBuiltins

leanprover · Dec 15, 2022 · 7c29cc7 · 7c29cc7
1 parent 52d00e8
commit 7c29cc7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
@@ -203,7 +203,7 @@ where
       else
         return .none
 
-@[inline] def simpOnlyBuiltins : List Name := [``eq_self]
+@[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self]
 
 structure MkSimpContextResult where
   ctx              : Simp.Context

diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
@@ -49,7 +49,7 @@ Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
 [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
 [Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if _h : 1 ≤ x then x else 0 ==> True
-Try this: simp only [and_self, iff_self]
+Try this: simp only [and_self]
 [Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True
 Try this: simp only [my_thm]