Is Expr.isEq correct?

Stream: lean4

[Luiz Carlos Rumbelsperger Viana]

So, I was trying to check whether a simple expression "5 = 5" is an equality, but idk if I'm understanding Expr.isEq correctly.
Consider the following:

def aux : Expr := mkApp (mkApp  (mkConst `Eq) (mkNatLit 5)) (mkNatLit 5)  -- this is supposed to be "5 = 5"

#eval aux.isAppOfArity ``Eq 2 -- true
#eval aux.isEq --false
#eval aux.isAppOfArity ``Eq 3 --false

It seems that the arity of the expression should be 2, but isEq is implemented assuming arity 3.
Is this correct? If so, what is the idea?

[Reid Barton]

Eq has an implicit type argument (here Nat) as well, which seems to be missing from your aux