Zulip Chat Archive

Stream: new members

Topic: Introducing myself + Naming Conventions

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:

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?

Damiano Testa (Nov 21 2020 at 10:35):


"Consequence of", maybe?

Eric Wieser (Nov 21 2020 at 10:40):

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

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?

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

Ruben Van de Velde (Nov 21 2020 at 10:49):

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

Mario Carneiro (Nov 21 2020 at 10:59):

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

Mario Carneiro (Nov 21 2020 at 11:00):

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

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

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

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)

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.

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: Dec 20 2023 at 11:08 UTC