RFC: Custom anonymous constructor syntax and structure construction

Proposal

Over at Mathlib we often run into the following situation (see Example below):

1. A general definition GeneralDef with constructor.
2. A specialised definition SpecialDef which is a special case (say α := Bool), say def SpecialDef := GeneralDef (α := Bool).
3. Then we need specialised projections and constructor(s) for SpecialDef, often named SpecialDef.mk

I propose:

1. We enable some syntax to prioritise the special constructor SpecialDef.mk so that we can use ⟨a, b, c⟩ to mean SpecialDef.mk a b c.
2. We make this work with where as well.

For example, we now have @[eliminator] to indicate the preferred recursor that the tactics cases and induction use.

Example

1. CategoryTheory.Limits.Cone is the general definition.
2. CategoryTheory.Limits.PullbackCone is a special case.
3. CategoryTheory.Limits.PullbackCone.mk is the custom constructor.

Community Feedback

1. #lean4 > Custom Constructor
2. #mathlib4 > Custom structure constructors with where where another syntax where (mk := name) is discussed.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the proposal and its linked Zulip discussions on custom constructors and where syntax, then inspect the existing @[eliminator] feature referenced in the issue. Done would require an agreed syntax and implementation that supports prioritised anonymous constructors and structure construction with where, including the PullbackCone-style example.