## 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:
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?

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

Hi!

"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: May 12 2021 at 23:13 UTC