Lets say I have a lemma FOO, is there way to generate dependeny graph (visual or data) in coq saying which lemmas are used to prove this lemma ?

Also is there some kind of warning system for dead code/dead lemmas ?

Would https://github.com/coq-community/coq-dpdgraph fit the bill?

yes looks like what I need.

Last updated: Jun 23 2024 at 03:02 UTC