5.1 Displaying
5.1.1 Print qualid.
This command displays on the screen informations about the declared or
defined object referred by qualid.
Error messages:
-
qualid not a defined object
Variants:
-
Print Proof qualid.
This is a synonym to Print qualid when qualid denotes a global constant.
5.1.2 Print All.
This command displays informations about the current state of the
environment, including sections and modules.
Variants:
-
Inspect num.
This command displays the num last objects of the current
environment, including sections and modules.
- Print Section ident.
should correspond to a currently open section, this command
displays the objects defined since the beginning of this section.
- Print.
This command displays the axioms and variables declarations in the
environment as well as the constants defined since the last variable
was introduced.