Zulip Chat Archive

Stream: new members

Topic: How to make @[reducible] work


view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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