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