Scott Morrison (May 01 2022 at 05:58):
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 (May 02 2022 at 10:38):
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.
Last updated: Aug 03 2023 at 10:10 UTC