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):
use_class will be useless outside of this section, right? Can you make it
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