Stream: Miscellaneous

Topic: Linter for unused hypotheses

view this post on Zulip 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?

view this post on Zulip 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: Jun 13 2024 at 03:02 UTC