## Stream: general

### Topic: type ascription style

#### Kenny Lau (Apr 28 2020 at 16:21):

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 (Apr 28 2020 at 17:26):

Which one elaborates faster?

I have no idea

#### Kevin Buzzard (Apr 28 2020 at 17:31):

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

#### Kenny Lau (Apr 28 2020 at 17:32):

I believe Chris meant in general.

#### Mario Carneiro (Apr 28 2020 at 22:53):

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

Last updated: May 15 2021 at 02:11 UTC