		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-show-only

Process the :show-only input.

Signature
(defarbrec-process-show-only show-only ctx state) → (mv erp nothing state)
Returns: nothing — Always nil.

Definitions and Theorems

Function: defarbrec-process-show-only

(defun defarbrec-process-show-only (show-only ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'defarbrec-process-show-only))
    (declare (ignorable __function__))
    (ensure-value-is-boolean$ show-only
                              "The :SHOW-ONLY input" t nil)))