Zulip Chat Archive

Stream: new members

Topic: Introducing myself + Naming Conventions


view this post on Zulip David Blitz (Nov 21 2020 at 10:31):

I'm David a hobby mathematician from Berlin, DE. I finished the Natural Number Game in my web browser and just installed lean to play the lost levels.
I've got a quick question concerning the Natural Number Game:
In

theorem lt_of_lt_of_le {a b c : mynat} : a < b  b  c  a < c :=

and in similar definitions,
why is an 'arrow' between types translated to '_of_' in natural language?

view this post on Zulip Damiano Testa (Nov 21 2020 at 10:35):

Hi!

"Consequence of", maybe?

view this post on Zulip Eric Wieser (Nov 21 2020 at 10:40):

I assume the rationale is similar to how person -> name could be called name_of_person.

view this post on Zulip David Blitz (Nov 21 2020 at 10:45):

Oh true, that makes sense. I think, I was confused by the translation switching 'source' and 'target' of the 'arrow'. I guess you could say I was expecting a co-variant translation ;) Is this a standard convention in lean?

view this post on Zulip Rémy Degenne (Nov 21 2020 at 10:47):

AFAIK, the standard convention is to name your theorem by its conclusion. The _of_ and the hypotheses are often absent if they are obvious

view this post on Zulip Ruben Van de Velde (Nov 21 2020 at 10:49):

And yeah, "of" is a standard mathlib #naming convention

view this post on Zulip Mario Carneiro (Nov 21 2020 at 10:59):

I read it more like "from", although I grant that the prepositions are not interchangeable

view this post on Zulip Mario Carneiro (Nov 21 2020 at 11:00):

mostly it's just a naming convention because if was taken

view this post on Zulip Mario Carneiro (Nov 21 2020 at 11:01):

and it pays to be short because this is certainly the number 1 most common label segment in mathlib

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 12:49):

I was always confused about why A_of_B_of_C meant B -> C -> A but actually when it comes to writing code this convention does seem to work quite well, you always know your goal and then you think of the hypotheses in order

view this post on Zulip David Blitz (Nov 21 2020 at 13:15):

@Kevin Buzzard Maybe it could be beneficial to explain this naming convention and its quirks in the Natural Number Game when it first pops up? (I think in Level 8 of Advanced Addition World)

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 13:16):

The whole game needs a tidy-up really. I just leave it because currently it works well enough and I'm busy with other projects. I wrote it because I was teaching this stuff.

view this post on Zulip David Blitz (Nov 21 2020 at 13:24):

I have to say that I really enjoyed the game as it is already. But I'll maybe create an issue for an explanation of the '_of_' naming convention in the game on github.


Last updated: May 12 2021 at 23:13 UTC