Set-raw-proof-format
Proof output with runes as lists and maybe clausal goals
General Forms:
(set-raw-proof-format t)
:set-raw-proof-format t
(set-raw-proof-format nil)
:set-raw-proof-format nil
(set-raw-proof-format :clause)
:set-raw-proof-format :clause
This command affects output from the theorem prover only when 'prove
output is not inhibited (see set-inhibit-output-lst) and gag-mode is
off (see set-gag-mode). The default behavior is obtained with argument
nil.
Calling this macro with argument t will cause simplification steps
from proof output, including steps from preprocess (see simple), to
print the list of runes used in a list format, rather than in the English
proof commentary. This ``raw'' format can be handy when you want to use that
list as a basis for hints that you construct for a subsequent proof
attempt.
Calling this macro with argument :clause provides not only the
behavior described above for argument t, but also causes goals to be
printed using their internal clausal format: each goal is a list, implicitly
disjoined, of translated terms. See clause.
To obtain the current raw proof format value of t, :clause or
nil, corresponding to the descriptions above, evaluate (@
raw-proof-format).
