SET-PRINT-CLAUSE-IDS

cause subgoal numbers to be printed when 'prove output is inhibited 
Major Section:  SWITCHES-PARAMETERS-AND-MODES


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 print-clause-id-okp print-clause-id-okp-level-4)