attribute [local simp]

Stream: mathlib4

[Reid Barton]

Does this syntax really exist? Never would have guessed

[Henrik Böving]

I don't know from the top of my head whether local simp is an attribute but yes in general you can add any kind of attribute after the fact with this syntax.

[Reid Barton]

In Lean 3 it was local attribute [simp]. To me it looks like we are adding the local attribute, and the simp attribute--probably in error.

[Reid Barton]

But I see it occurs many times already.

[Sebastian Ullrich]

local and scoped are attribute modifiers, so you can also use [foo, local bar, ...]