fix: mark imp_eq as a pre-theorem

leanprover · Dec 24, 2024 · bb339e1 · bb339e1
1 parent 6b8caf7
commit bb339e1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
@@ -41,7 +41,7 @@ attribute [grind_norm] not_true
 attribute [grind_norm] not_false_eq_true
 
 -- Implication as a clause
-@[grind_norm] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
+@[grind_norm↓] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
 -- And