Finding the `@[simp]` attribute

Stream: general

[Eric Wieser]

I'm struggling to work out why this works:

example : [].rightpad 0 0 = [] := by
  simp? -- simp only [List.rightpad, ...]

Where is src#List.rightpad being marked as simp? docs#List.rightpad doesn't indicate that it is.

[Eric Wieser]

In this case it seems the attribute is in a later file; should this be discouraged?

[Kim Morrison]

https://github.com/leanprover/lean4/pull/11928