		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-input-processing

Deftreeops-process-print

Process the :print input.

Signature
(deftreeops-process-print print) → (mv erp print)
Returns: print — Type (evmac-input-print-p print).

Definitions and Theorems

Function: deftreeops-process-print

(defun deftreeops-process-print (print)
 (declare (xargs :guard t))
 (let ((__function__ 'deftreeops-process-print))
  (declare (ignorable __function__))
  (b*
   (((reterr) :error)
    ((unless (and print (evmac-input-print-p print)))
     (reterr
      (msg
       "The :PRINT input ~x0 must be ~
                      :ERROR, :RESULT, :INFO, or :ALL."
       print))))
   (retok print))))

Theorem: evmac-input-print-p-of-deftreeops-process-print.print

(defthm evmac-input-print-p-of-deftreeops-process-print.print
  (b* (((mv acl2::?erp common-lisp::?print)
        (deftreeops-process-print print)))
    (evmac-input-print-p print))
  :rule-classes :rewrite)