Stream: Coq users

Topic: Lemmas in a Module/File

Mycroft92 (Oct 28 2021 at 09:42):

Hi,
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>."

Théo Winterhalter (Oct 28 2021 at 09:47):

You can use Print on a module.

Théo Winterhalter (Oct 28 2021 at 09:48):

It might not be exactly what you want though, I'm not sure.

Mycroft92 (Oct 28 2021 at 09:50):

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.

Théo Winterhalter (Oct 28 2021 at 09:51):

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?

Mycroft92 (Oct 28 2021 at 09:54):

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: Oct 13 2024 at 01:02 UTC