Zulip Chat Archive

Stream: general

Topic: type ascription style


view this post on Zulip 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)

view this post on Zulip Chris Hughes (Apr 28 2020 at 17:26):

Which one elaborates faster?

view this post on Zulip Kenny Lau (Apr 28 2020 at 17:26):

I have no idea

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 28 2020 at 17:32):

I believe Chris meant in general.

view this post on Zulip 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