## 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: May 15 2021 at 23:13 UTC