norm_num lemma function equalities

Stream: metaprogramming / tactics

[Markus Himmel]

I am currently trying to understand the changes introduced in #4048. I think I understand the basic idea of the change, but I'm confused about the details. Here's the statement docs#Mathlib.Meta.NormNum.isInt_sub:

theorem isInt_sub {α} [Ring α] : ∀ {f : α → α → α} {a b : α} {a' b' c : ℤ},
    f = HSub.hSub → IsInt a a' → IsInt b b' → Int.sub a' b' = c → IsInt (f a b) c

This makes sense to me: the subtraction in the conclusion is replaced by f. On the other hand, docs#Mathlib.Meta.NormNum.isInt_mul looks like this:

theorem isInt_mul {α} [Ring α] : ∀ {f : α → α → α} {a b : α} {a' b' c : ℤ},
    f = HMul.hMul → IsInt a a' → IsInt b b' → Int.mul a' b' = c → IsInt (a * b) c

Here, the function f is introduced but not used in the conclusion. Should the conclusion of this lemma be IsInt (f a b) c?