Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
There are commands to list required files (Print Libraries.), available constants (Search), but as far as I know, there is none to print currently available modules (which should probably include the libraries).
Proposed solution
I propose, as an easy and (hopefully) not so controversial solution, to add:
Print Modules (which should also probably display functors)
Print Module Types (which should also probably display functor types)
Alternative solutions
Another possible solution would be to have something more elaborate like Search, e.g.
SearchModule "Nat". (* display all module whose name contains `Nat` *)
Is your feature request related to a problem?
There are commands to list required files (
Print Libraries.), available constants (Search), but as far as I know, there is none to print currently available modules (which should probably include the libraries).Proposed solution
I propose, as an easy and (hopefully) not so controversial solution, to add:
Print Modules(which should also probably display functors)Print Module Types(which should also probably display functor types)Alternative solutions
Another possible solution would be to have something more elaborate like
Search, e.g.or, maybe
Additional context
No response