What's the binding power of →?

Stream: general

[Kevin Buzzard]

#print notation → doesn't tell me, presumably because it's not notation. I was trying to verify without looking at the source code that P ∧ Q → R was indeed parsed as (P ∧ Q) → R.

[Kevin Buzzard]

Aah, got it. From https://leanprover.github.io/reference/other_commands.html#notation-declarations (even though I don't think it's notation) "The implication arrow binds with strength 25"