Custom Constructor

Stream: lean4

[Kenny Lau]

Over at Mathlib we often run into the following situation:

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'm wondering whether we can 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.

For example, we now have (i forgot the name) syntax to indicate the preferred recursor that the tactic induction uses.

[Kenny Lau]

(Example: CategoryTheory.Limits.PullbackCone is a special case of CategoryTheory.Limits.Cone, with special constructor CategoryTheory.Limits.PullbackCone.mk.)

[Kenny Lau]

Update: I would also like the where thing to work with SpecialDef.mk as well

[Kim Morrison]

Could you write an RFC, please?

[Bhavik Mehta]

Kenny Lau said:

Update: I would also like the where thing to work with SpecialDef.mk as well

Previous discussion on this here: #mathlib4 > Custom structure constructors with `where`

[Kenny Lau]

@Kim Morrison @Bhavik Mehta lean4#10412