difference between `+` and `HAdd.hAdd`

Stream: new members

[nnarek]

I was thinking that a+b is just a macro/notation which maps to HAdd.hAdd a b
but I see that these two terms have different behavior. lean4 is not able to synthesize class for first one, but is able for second one.
I am expecting same behavior because I just unwrapped + macro

#check ∀ (a: Nat -> Nat) (n : Nat), a n = HAdd.hAdd (HMul.hMul 3 n) (HPow.hPow (Neg.neg (1 : Int)) n)
#check ∀ (a: Nat -> Nat) (n : Nat), a n = (HMul.hMul 3 n) + (HPow.hPow (Neg.neg (1 : Int)) n)

[Alex Meiburg]

It is very very close to "just" a macro/notation, but it has to do with the order that implicit arguments are inferred, and casts inserted. The issue that you'll see in that example is that you're getting

↑(a n) = ↑(3 * n) + (-1) ^ n

in the second example, so two coercions being inserted. It found an Add instance of Int (using the last term as a guide) and then inferred the other ones based on that, adding coercions. But in

HAdd.hAdd (HMul.hMul 3 n) (HPow.hPow (Neg.neg (1 : ℤ)) n)

it first finds that the first argument is a Nat, and the second argument is an Int, and so it gets stuck looking for HAdd ℕ ℤ ?..

[Kenny Lau]

@nnarek you have too much other stuff getting in the way of simply checking whether they're the same, if you make the situation as simple as possible then you can clearly see that they are the same thing:

-- set_option pp.all true
#check 3 + 4 -- 3 + 4
#check HAdd.hAdd 3 4 -- 3 + 4

[nnarek]

Thank you, so I need to insert coerection manually

#check ∀ (a: Nat -> Nat) (n : Nat), a n = HAdd.hAdd ↑(HMul.hMul 3 n) (HPow.hPow (Neg.neg (1 : Int)) n)

[Robin Arnez]

a + b elaborates to binop% HAdd.hAdd a b which is similar to HAdd.hAdd a b but has different handling of coercions