type ascription style

Stream: general

[Kenny Lau]

Let's decide once-and-for-all whether we want (2 ^ 4 : \R) or (2 : \R) ^ 4. I prefer the former because this is more in line with Lean's elaboration style (outside-in / from left to right / traversal)

[Chris Hughes]

Which one elaborates faster?

[Kenny Lau]

I have no idea

[Kevin Buzzard]

They both elaborate in about 1ms on my laptop and it seems to be random which one is quicker

[Kenny Lau]

I believe Chris meant in general.

[Mario Carneiro]

I think that we shouldn't have a style guide for this. Use whatever makes lean happy; it helps to know lean's elaboration order when trying to make lean happy, but if they both work then they are both okay