Koundinya Vajjha (Jan 25 2022 at 20:18): Koundinya Vajjha (Jan 25 2022 at 20:18):Hi all,
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?
Ali Caglayan (Jan 25 2022 at 20:32):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: Apr 20 2024 at 01:41 UTC