nolinting generated decls

Stream: std4

[Matthew Ballard]

How do I nolint simpNF the declarations generated by @[simps]? Just @[simps, nolint simpNF] doesn’t work. See !4#2198 for an example where we have a false positive but I don’t know a way to turn off the linter.

Other discussion at

• #mathlib4 > CategoryTheory.Adjunction.Basic
• #mathlib4 > simps and simpNF linter

[Matthew Ballard]

Would it make sense to register a global option for this?

[Floris van Doorn]

You can use attribute [nolint simpNF] generated_decl

[Matthew Ballard]

Thanks I will try that.