exponential object notation precedence

Stream: mathlib4

[Mario Carneiro]

A ⨯ B ⟹ C parses as A ⨯ (B ⟹ C), I think ⨯ needs its precedence to be raised... It might be good to review all of these operators and make sure they match the corresponding operators on Type

[Johan Commelin]

I would expect it to parse as $(A \times B) \to C$. On the other hand, the current parsing is consistent with "exponentiation before multiplication".