naming convention diagram

Stream: mathlib4

[Derek Rhodes]

I couldn't find a diagram that quickly shows how the abbreviated aspect of the naming convention works, so I whipped one up for anyone who might want to use it.

image.png

[Edward van de Meent]

this makes me realise that you might miss this when searching for of_inv_mul_eq rather than of_eq_inv_mul... is there a reason why one would be preferred over the other?

[Derek Rhodes]

Not sure, but the identified relations/operations appear to be referenced in order from left to right.

[Derek Rhodes]

there is some rationale given on this page

[Edward van de Meent]

my question was more about why the argument is shaped the way it is, rather than why the name is what it is...

[Eric Wieser]

I think this would be clearer if you wrote the name above the statement, rather than on one line

[Derek Rhodes]

@Eric Wieser Yeah, I agree, but I think the name would need to be mirror imaged for all the lines to be somewhat vertical, but I'll try it and see how it looks.

[Yaël Dillies]

I actually really that diagram!

[Derek Rhodes]

Thanks! I think for the theorem name to vertically placed, it would need to be split around the _of_,

image.png

[Kevin Buzzard]

I thought "of" was the colon!

[Eric Wieser]

the one after h, you mean?

[Damiano Testa]

I always interpreted it as "now that we described the goal, let's disambiguate by describing the assumptions!". :upside_down:

[Kevin Buzzard]

The one before the goal, because I remember learning that you can replace an implies by moving the hypothesis before the colon. But the argument isn't good because the colon doesn't disappear if you replace it by an implies, it just moves.

[Eric Wieser]

I think foo_of_bar_of_baz is prescribed by our naming convention for Bar -> Baz -> Foo, so I don't think that rule works

[Kevin Buzzard]

Indeed there are problems with multiple ofs

[Edward van de Meent]

i think of is just mirrored -> (i.e. <- with the opposite associativity from ->)

[Eric Wieser]

That doesn't match my example above

[Edward van de Meent]

ah, you're right!

[Kevin Buzzard]

Jeremy explained the of logic to me years ago and I believe that it's a good choice pragmatically, although it will lead to very confusing-looking diagrams if you start explaining it using diagrams. The idea is that you're first thinking about the conclusion and then all the hypotheses in order, so that's what the naming convention should mimic.