Is there a way to inspect/print the Lemmas listed in one of the imports? I keep confusing in my naming convention and would like to check quickly.
Is there an explicit command that does this? Say "Print Lemma <filename/ModuleName>."
You can use
It might not be exactly what you want though, I'm not sure.
Thanks @Théo Winterhalter . I wanted only the names, without the type annotations and preferably filtered on functions/Theorems since the complete log is too long.
I guess you could always parse the result yourself but I'm not sure it's worth the effort. If it's only about naming convention, reading a few names should be enough?
Yeah true. It does lift some of my confusion I guess. I was hoping for a condensed form "x, y, z" of solution. You are right that it might not be worth the effort.
Last updated: Jan 29 2023 at 05:03 UTC