Custom name for projection in `structure extends`

Stream: lean4

[Andrew Yang]

Is it possible to rename the custom name for projection (the toFoo) in structure extends?
For context, I'm trying to make Scheme.Hom extends LocallyRingedSpace.Hom extends PresheafedSpace.Hom, the LocallyRingedSpace.Hom-> PresheafedSpace.Hom gets called toHom, and the Scheme.Hom -> LocallyRingedSpace.Hom now becomes toHom_1, and the extra _ is pissing off simps.

[Yaël Dillies]

I hit the same issue in #10560 with toMinimalAxioms and toMinimalAxioms_1

[Andrew Yang]

Okay the name seems to be hardcoded at Lean.Elab.Command.mkToParentName. IIRC we could write
structue Foo extends (myBar : Bar) in lean3 to rename the projections. Could we somehow restore this behaviour?

[Joachim Breitner]

Can you give a nicer alternative name using a manual abbrev?
Ah, but too late for simps, I assume.

Certainly worth recording as a lean issue, especially if it's a regression relative to lean 3. Maybe also try to assess just how pressing this is for mathlib (relative to all the other things that could be worked on :man_shrugging:)

[Andrew Yang]

Is there still an online playground to test lean3 somewhere? If I was not hallucinating about that lean3 syntax I'll open an issue.
Anyways I'll start looking into simps to see if things can be improved from that side. Maybe a solution here is for simps to not consider A as a prefix of B if B = A_someNumber.

[Joachim Breitner]

That sounds useful too

[Andrew Yang]

@Floris van Doorn does the workaround for simps above sound reasonable? I could try to implement it if it is. (It would be better done by you but I assume you are busy with Carleson.)

[Eric Wieser]

Andrew Yang said:

Is there still an online playground to test lean3 somewhere? If I was not hallucinating about that lean3 syntax I'll open an issue.

Zulip should add a Lean 3 playground link to this

structure my_prod extends to_base : prod nat Nat

[Andrew Yang]

I opened a tentative PR for the simps workaround #15095