Zulip Chat Archive

Stream: general

Topic: initialize_simps_projections for inductive types

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: Dec 20 2023 at 11:08 UTC