5.1 Displaying
5.1.1 Print ident.
This command displays on the screen informations about the declared or defined object ident.Error messages:
- ident not declared
Variants:
-
Print Proof ident.
In case ident corresponds to an opaque theorem defined in a section, it is stored on a special unprintable form and displayed as <recipe>. Print Proof forces the printable form of ident to be computed and displays it.
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.