Zulip Chat Archive

Stream: new members

Topic: How to make @[reducible] work


Sebastián Galkin (Aug 25 2020 at 02:44):

Is there a trick to make reducible attribute work? I'm marking a pretty simple definition as reducible, and yet, I need to manually unfold every time.

Does it only work for certain types of definitions?

Scott Morrison (Aug 25 2020 at 03:23):

Why do you want it reducible in the first place? (The first thing to be sure of is that you may want to have @[simp] lemmas instead.)

Scott Morrison (Aug 25 2020 at 03:23):

What are you doing when you manually unfold it?


Last updated: Dec 20 2023 at 11:08 UTC