		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-proofs

Process the :proofs input.

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

Definitions and Theorems

Function: atc-process-proofs

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

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

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