I have proved a fairly large theorem which has a large number of hypotheses. Is there a way (say using Ltac) that I can check if some hypotheses are unused in the final proof?
One way that comes to mind is to put all your hypotheses in a section using
Context. That way when you close the section, coq will not include unused hypotheses. Then you can clearly see using
About what the correct type for the theorem should be.
Last updated: Aug 14 2022 at 11:02 UTC