Zulip Chat Archive

Stream: general

Topic: Linter rejects automatic instance


Bhavik Mehta (Apr 17 2020 at 21:50):

In the following file, the unused arguments linter complains about #print f.decidable_eq /- argument 2: [a : decidable_eq J] -/ having an unused argument - is it possible to change how the derive works to avoid this?

import tactic

variable (J : Type)

def mytype (J : Type) : Type := option J

@[derive decidable_eq]
inductive f : mytype J  Type
| a : f none

#lint

Bhavik Mehta (Apr 20 2020 at 22:10):

Cf my PR https://github.com/leanprover-community/mathlib/pull/2461

Kevin Buzzard (Apr 20 2020 at 22:14):

hmm I think this might be a known issue

Scott Morrison (Apr 20 2020 at 23:40):

@Bhavik Mehta, could you create an issue for this? We should track it.

Bhavik Mehta (Apr 20 2020 at 23:41):

Looking at https://github.com/leanprover-community/mathlib/issues/1077, it seems to be a lean issue rather than a mathlib issue...

Bryan Gin-ge Chen (Apr 21 2020 at 00:09):

Is there a related open issue on the community Lean repository?

Bhavik Mehta (Apr 21 2020 at 00:10):

Doesn't seem like it

Kevin Buzzard (Apr 21 2020 at 08:14):

Sorry, when I said known issue I literally just meant "I think someone mentioned it on the chat once". I forgot that an issue was a real thing

Rob Lewis (Apr 21 2020 at 08:18):

This is unrelated to #1077. For now you can do attribute [nolint unused_arguments] f.decidable_eq. This is probably fixable, probably not trivial. The decidable_eq derive handler is in core so it's an issue there.


Last updated: Dec 20 2023 at 11:08 UTC