How to make @[reducible] work

Stream: new members

[Sebastián Galkin]

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]

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]

What are you doing when you manually unfold it?