		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-keep-going

Process the :keep-going input.

Signature
(input-files-process-keep-going keep-going) → (mv erp new-keep-going)
Returns: new-keep-going — Type (booleanp new-keep-going).

Definitions and Theorems

Function: input-files-process-keep-going

(defun input-files-process-keep-going (keep-going)
 (declare (xargs :guard t))
 (let ((__function__ 'input-files-process-keep-going))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((unless (booleanp keep-going))
     (reterr
      (msg
       "The :KEEP-GOING input must be a boolean ~
                      but it is ~x0 instead."
       keep-going))))
   (retok keep-going))))

Theorem: booleanp-of-input-files-process-keep-going.new-keep-going

(defthm booleanp-of-input-files-process-keep-going.new-keep-going
  (b* (((mv acl2::?erp ?new-keep-going)
        (input-files-process-keep-going keep-going)))
    (booleanp new-keep-going))
  :rule-classes :rewrite)