LP, the Larch Prover -- The display command

The display command displays information about LP's logical system.

Syntax

<display-command>  ::= display [ <information-type> ] [ <names> ]
<information-type> ::= classes | conjectures | facts | names
                          | ordering-constraints | proof-status | symbols

Examples

display
display *Hyp
display ordering-constraints contains-operator(+)

Usage

The display command displays information of the requested <information-type> about all facts and conjectures with names matching <names>. If <information-type> is omitted, it is assumed to be facts.
display classes
Displays the definitions of all <class-name>s.

display conjectures [ <names> ]
Displays all unproved conjectures [with the specified names].

display facts [ <names> ]
Displays all facts in the current proof context [with the specified names]. Indicates immune facts by an (I) following their names, ancestor-immune statements by an (i), and passive facts by a (P).

display names
Displays all name-prefixes introduced in the current proof context.

display ordering-constraints [ <names> ]
Displays the registry for all operators [in the named facts] in the current proof context, unless the value of the ordering-method setting is polynomial, in which case it displays the polynomial interpretations of these operators.

display proof-status
Displays the status of the current conjecture and all other conjectures for which it is a subgoal (of a subgoal ...).

display symbols [ <names> ]
Displays all sorts, operators, and variables [in the named facts] in the current proof context. The command display symbols displays all symbols in the current proof context, whereas display symbols * only displays those that occur in some fact.