		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-header

Process the :header input.

Signature
(atc-process-header options) → (mv erp header)
Arguments: options — Guard (symbol-alistp options).
Returns: header — Type (booleanp header).

Definitions and Theorems

Function: atc-process-header

(defun atc-process-header (options)
 (declare (xargs :guard (symbol-alistp options)))
 (let ((__function__ 'atc-process-header))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    (header-option (assoc-eq :header options))
    (header (if header-option (cdr header-option)
              nil))
    ((unless (booleanp header))
     (reterr
      (msg
       "The :HEADER input must be a boolean, ~
                      but ~x0 is not a boolean."
       header))))
   (retok header))))

Theorem: booleanp-of-atc-process-header.header

(defthm booleanp-of-atc-process-header.header
  (b* (((mv acl2::?erp acl2::?header)
        (atc-process-header options)))
    (booleanp header))
  :rule-classes :rewrite)