Set-print-clause-ids
Cause subgoal numbers to be printed when 'prove output is
inhibited
General Forms:
(set-print-clause-ids t)
:set-print-clause-ids t
(set-print-clause-ids nil)
:set-print-clause-ids nil
This command affects output from the theorem prover only when 'prove
output is inhibited (see set-inhibit-output-lst) or gag-mode is on (but
in that case the :goals setting issues this command automatically; see
set-gag-mode). Calling this macro with value t as shown above
will cause subsequent proof attempts with 'prove output inhibited to
print the subgoal number, so that you can see the progress of the proof; value
nil reverts to the default behavior, where this is not the case. On a
related note, we point out that you can cause output to be saved for later
display; see pso and see pso!.
If 'prove output is inhibited or gag-mode is on, and if you issue
(set-print-clause-ids t) (either explicitly or with (set-gag-mode
:goals)), then you can restrict when subgoal numbers are printed. In the
following example we restrict to subgoals that are no more than four
inductions deep, no more than four casesplits deep, and no more than four
single-subgoals deep. For additional relevant explanation, see clause-identifier and see defattach.
(defun print-clause-id-okp-level-4 (cl-id)
(declare (xargs :mode :logic :guard (clause-id-p cl-id)))
(and (<= (length (access clause-id cl-id :pool-lst))
4)
(<= (length (access clause-id cl-id :case-lst))
4)
(<= (access clause-id cl-id :primes)
4)))
(defattach-system print-clause-id-okp print-clause-id-okp-level-4)
