defLemma failing when it seems it shouldn't

Stream: mathlib4

[Thomas Murrills]

When does the defLemma linter fail or not? For example, I have one definition whose return type is a structure with a single equality argument, and that's fine. But if the return type is a structure with one data field and one equality argument, that's not. Is this a relevant factor?

[Thomas Murrills]

If I replace theorem with def, I get a much scarier error:

unsupported Mathlib.Meta.NormNum.IsNat.casesOn application during code generation

[Thomas Murrills]

I'm wondering if this warrants a [nolint defLemma].

[Johan Commelin]

Could you please link to a line of code?

[Thomas Murrills]

This particular issue was worked around on mathlib4#1441, so I guess it doesn't matter anymore! :)