chore: mark Mul.mul and HMul.hMul as match_pattern

allows fixing regressions in mathlib introduced in nightly-2024-02-25
leanprover · Jan 30, 2025 · 49e3bf5 · 49e3bf5
1 parent e922edf
commit 49e3bf5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
@@ -1551,7 +1551,7 @@ instance instAddNat : Add Nat where
 
 /- We mark the following definitions as pattern to make sure they can be used in recursive equations,
    and reduced by the equation Compiler. -/
-attribute [match_pattern] Nat.add Add.add HAdd.hAdd Neg.neg
+attribute [match_pattern] Nat.add Add.add HAdd.hAdd Neg.neg Mul.mul HMul.hMul
 
 set_option bootstrap.genMatcherCode false in
 /--