		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-files

Process the :files input.

Signature
(input-files-process-files files-presentp files) → (mv erp new-files)
Arguments: files-presentp — Guard (booleanp files-presentp).
Returns: new-files — Type (string-listp new-files).

Definitions and Theorems

Function: input-files-process-files

(defun input-files-process-files (files-presentp files)
 (declare (xargs :guard (booleanp files-presentp)))
 (let ((__function__ 'input-files-process-files))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((unless files-presentp)
     (reterr
      (msg
       "The :FILES input must be supplied, ~
                      but it was not supplied.")))
    ((unless (string-listp files))
     (reterr
      (msg
       "The :FILES input must evaluate to a list of strings, ~
                      but it evaluates to ~x0 instead."
       files)))
    ((unless (no-duplicatesp-equal files))
     (reterr
      (msg
       "The :FILES input must be a list without duplicates, ~
                      but the supplied ~x0 has duplicates."
       files)))
    ((unless (consp files))
     (reterr
      (msg
       "The :FILES input must contain at least one element, ~
                      but it does not contain any."))))
   (retok files))))

Theorem: string-listp-of-input-files-process-files.new-files

(defthm string-listp-of-input-files-process-files.new-files
  (b* (((mv acl2::?erp ?new-files)
        (input-files-process-files files-presentp files)))
    (string-listp new-files))
  :rule-classes :rewrite)