Infix Delaborator Bug?

Stream: lean4

[Mac]

I was trying out a new way to specify mixfix notation and I encounter the following oddity:

notation "(+)" => HAdd.hAdd
infixl:65 (priority := default + default) " + " => (+)
#check 2 + 2
/-
  (+) : Nat
-/

That is, 2 + 2 doesn't delab properly (the operands get completely wiped out). Is this a bug? Or is it an expected pitfall of my approach? If it is, in fact, a bug, I'll go create an issue for it on GitHub.

[Sebastian Ullrich]

Yes, this does look like a bug

[Mac]

k, I will go make a proper issue