to_isSomePropStructure

Stream: mathlib4

[Winston Yin (尹維晨)]

In the current naming scheme, there's a discrepancy in naming fields/theorems under Prop structures. Say we have three structures: IsFoo, IsFooBar extending IsFoo, and IsBar, all of which are Prop. Automatically we have the field IsFooBar.toIsFoo. Then, we want to state lemma IsFooBar.to_isBar : IsBar. Ah you see, this is a proof, so we need to use lower camel case to_isBar, which looks inconsistent with toIsFoo.

Maybe we don't care at all, but I just wanted to mention it here as I'm porting deprecated.group, and there's a bunch of these...

[Yaël Dillies]

I don't understand why we want toSomeTypeStructure instead of to_someTypeStructure either.

[Yaël Dillies]

The to is not part of the structure name, so surely it shouldn't fall into the same part of the name?

[Ruben Van de Velde]

I think maybe toFoo is what lean comes up with for extends?

[Yaël Dillies]

Indeed. And for the above reason I think it's bad.

[Ruben Van de Velde]

I think it's valuable to match the extends convention, but I don't really care what convention that ends up being

[Thomas Murrills]

Yaël Dillies said:

I don't understand why we want toSomeTypeStructure instead of to_someTypeStructure either.

For structures which are Types, I think it should definitely be toSomeTypeStructure; terms valued in a Type should be lower camel case, and underscores shouldn’t appear. For terms, underscores ⇒ proof-like now!

I don’t think it’s the worst thing if we have a special case to match the extends convention, even if it goes against the naming convention. You sort of think of to* names as special actions on structures anyway, and not as something “proof-like”. …well, I do, anyway! :)

Plus, you should be able to guess the name of a projection knowing the types of the involved structures alone even if you don’t know how the diamond works out, so they should all at least be consistent; if we were to change it at all I think it would make sense to do so in core so that every to-projection to a Prop structure like this was named in lower_snakeCase.