Naming `structure` parent projections

Stream: lean4

[Kyle Miller]

RFC: lean4#7099

The short version is that it would be nice to make the algorithm for parent projection names be more deterministic. A way to do that is to have it be that for a parent S .., the projection by default is toS, and otherwise you can supply a name with the syntax

structure T extends toTheS : S

However, there's a wrinkle, which is that this is ambiguous with the resultant type syntax

structure T extends P : Prop

I'd like to change this syntax to

structure T : Prop extends P

This is a breaking change, but it's more natural. The parents to a structure are not part of the type constructor. They're more akin to fields. The elaboration order for structure goes binders, resultant type, parents, fields.

[Kyle Miller]

I'm able to make new syntax that still parses the old syntax and gives appropriate warnings/errors with how to update.

It's not great having a breaking change like this, but I'm hoping we can agree that the change would be net positive.