Zulip Chat Archive

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)


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


This works well, except that the linter complains:

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: Dec 20 2023 at 11:08 UTC