Email Gateway (Aug 18 2022 at 10:22): Email Gateway (Aug 18 2022 at 10:22):From: "Nikolaos S. Papaspyrou" <nickie@softlab.ntua.gr>
When generating the graph of theorem dependencies for a non-trivial theorem in a
quite large theory, one usually does not want to see all of his/her theorems
there. A concrete example: one may have a group of ten related minor lemmata
that are used in the proof of a large theorem. It would be nice if these ten
could be "grouped" together as a single node in the dependency graph.
At the moment, the only way I know to achieve this effect is to put the ten
lemmata in a separate theory. Wouldn't it be nice if the dependency graph could
understand, for example, the sectioning mechanism? Has anyone tried to do what
I suggest? Or have a different workaround?
Thanks,
Nikos.
Last updated: May 03 2024 at 12:27 UTC