'proveoutput 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 nilThis command affects output from the theorem prover only when
'proveoutput is inhibited (see set-inhibit-output-lst) or gag-mode is on (but in that case the
:goalssetting issues this command automatically; see set-gag-mode). Calling this macro with value
tas shown above will cause subsequent proof attempts with
'proveoutput inhibited to print the subgoal number, so that you can see the progress of the proof; value
nilreverts 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!.
'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)