initialize_simps_projections for inductive types

Stream: general

[Scott Morrison]

Is there any prospect of enabling @[simps] for inductive types? This was suggested at https://github.com/leanprover-community/mathlib/pull/13744#discussion_r860218917 by @Eric Wieser. As far as I understand, there's no easy way to make this work, so we won't hold up this PR for it, but I thought I'd check in with @Floris van Doorn on it.

[Floris van Doorn]

This is indeed not possible using the current implementation. It could be added, but it's not trivial. I'm not planning to add in it Lean 3, but I might be interested in doing it in Lean 4 at some point. I added it to #5489.