Zulip Chat Archive

Stream: general

Topic: incorrect_type_class_argument linter


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Rob Lewis (Jun 09 2020 at 16:01):

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

view this post on Zulip Reid Barton (Jun 09 2020 at 16:01):

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

view this post on Zulip Reid Barton (Jun 09 2020 at 16:04):

Why is it linting the autogenerated equational lemma?

view this post on Zulip Rob Lewis (Jun 09 2020 at 16:04):

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

view this post on Zulip 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.

view this post on Zulip 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