Stéphane Desarzens (May 21 2021 at 09:59): Stéphane Desarzens (May 21 2021 at 09:59):Let’s say I define something like Definition foo (m n o : nat) := m + n. Is there some way Coq can warn me, that I assumed o but didn’t use it in the term, so it could be eliminated?
I sometimes make the mistake of adding unnecessary terms to definitions or lemmas and such a warning would help me. It would also help during refactoring/rewriting.
Jason Gross (Jun 06 2021 at 02:25):The feature would be relatively easy to add (the spec is "emit a warning if when you Print const any of the leading lambdas has an argument that shows up as an underscore"), perhaps open an issue requesting this feature?
Jason Gross (Jun 06 2021 at 02:26):The kludgy way to get this is to strip all the type annotations off, and then Coq will complain that it can't infer the type of unused arguments (this may cause other problems though).
Last updated: Oct 13 2024 at 01:02 UTC