Priority for inner product notation

Stream: lean4

[Tomas Skrivan]

I have very little understanding how priorities work, what would be a good way to set up priority for 'inner product like' notation?

notation:100 "⟪" x:60 ", " y:61 "⟫" => Inner x y

but this does not work properly as function application does not work properly. Writing f ⟪x,x⟫ gives an error but f (⟪x,x⟫) works.

[Tomas Skrivan]

mwe:

def inner (x y : Nat) : Nat := x * y

notation:100 "⟪" x:60 ", " y:61 "⟫" => inner x y

#check (Nat.succ (⟪1,1⟫))   --- works
#check (Nat.succ ⟪1,1⟫)    --- error