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):
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: May 08 2021 at 04:14 UTC