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:
  1. qualid not a defined object

Variants:
  1. 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:
  1. Inspect num.
    This command displays the num last objects of the current environment, including sections and modules.
  2. Print Section ident.
    should correspond to a currently open section, this command displays the objects defined since the beginning of this section.
  3. Print.
    This command displays the axioms and variables declarations in the environment as well as the constants defined since the last variable was introduced.