print
The print
command allows the programmer to display an expression value in the console. The command is often used for debugging while developing a proof.
Syntax
print [expression];
The print
command begins with the keyword print
followed by a ;
terminated expression.
Behavior
If [expression]
evaluates to an object value, then the following is printed in the console:
'[file name]' line [line number]: [object identifier]
Where [object identifier]
is the identifier of the object referred to by the object value.
If [expression]
evaluates to a verified sentence value, then the following is printed in the console:
'[file name]' line [line number]: (verified) [sentence]
Where [sentence]
is the sentence referred to by the sentence value.
If [expression]
evaluates to a unverified sentence value, then the following is printed in the console:
'[file name]' line [line number]: (unverified) [sentence]
Where [sentence]
is the sentence referred to by the sentence value.
When a sentence is printed by the print
command, the sentence is printed in normal form. In normal form, each quantified or unbound object is replaced with numbers 0, 1, 2, etc. The nth unbound object is always renamed to the object n in the printed sentence value. Then the remaining quantified variables’ identifiers are replaced with the next available number.
Additionally, unbound predicates in normal form are denoted in order by P0
, P1
, P2
, etc.
Examples
The following command:
print trivial(<: true>);
Prints the following line in the console:
'[file name]' line [line number]: (verified) true
The following command:
print <Q(3), Z: *X*Y(Q(X, Y, Z) <-> Q(Z, X, Y))>
Prints the following line in the console:
'[file name]' line [line number]: (unverified) *1*2(P0(1, 2, 0) <-> P0(0, 1, 2))