## Stream: general

### Topic: incorrect_type_class_argument linter

#### Sebastien Gouezel (Jun 09 2020 at 15:57):

I would like to define something which is not a class, but use it as a class in a part of a development. Typically something like

import data.nat.basic

/-- Something which is not a class, but that I will use locally as a class -/
def not_class (n : ℕ) : Prop := (n = n)

section

local attribute [class] not_class

/-- I want to use not_class as a class here. -/
@[nolint incorrect_type_class_argument unused_arguments]
def use_class (n : ℕ) [not_class n] : ℕ := n

end


This works well, except that the linter complains:

/- INCORRECT TYPE-CLASS ARGUMENTS.
Some declarations have non-classes between [square brackets]: -/
#print use_class.equations._eqn_1 /- These are not classes. argument 2: [_inst_1 : not_class n] -/


What is the right way to tell the linter that, really, I know what I am doing here?

#### Rob Lewis (Jun 09 2020 at 15:59):

I guess use_class will be useless outside of this section, right? Can you make it private?

#### Rob Lewis (Jun 09 2020 at 16:01):

Hmm, private declarations seem to be included in that lint, that doesn't seem right.

#### Reid Barton (Jun 09 2020 at 16:01):

Maybe it would make more sense to just implement this test in Lean itself?

#### Reid Barton (Jun 09 2020 at 16:04):

Why is it linting the autogenerated equational lemma?

#### Rob Lewis (Jun 09 2020 at 16:04):

Some linters apply to all declarations including the autogenerated ones. This one probably shouldn't.

#### Sebastien Gouezel (Jun 09 2020 at 16:04):

Ideally, if I disable a linter for a def, then it should be disabled also for its equational lemmas.

#### Sebastien Gouezel (Jun 09 2020 at 16:42):

Thanks @Rob Lewis for #3006. Shortest (and most efficient) PR ever?

Last updated: May 14 2021 at 14:20 UTC