		Search-engine friendly clone of the ACL2 documentation.

Vl-read-files

Vl-read-files-aux

Tail recursive loop for vl-read-files.

Signature
(vl-read-files-aux filenames nrev &key (state 'state)) → (mv errmsg? nrev state)
Arguments: filenames — The files to read.
Guard (string-listp filenames).

You should never need to reason about this directly, because of the following rule:

Theorem: vl-read-files-aux-redef

(defthm vl-read-files-aux-redef
  (equal (vl-read-files-aux filenames acc)
         (b* (((mv errmsg data state)
               (vl-read-files filenames)))
           (mv errmsg (append acc data) state))))

Definitions and Theorems

Function: vl-read-files-aux-fn

(defun vl-read-files-aux-fn (filenames nrev state)
  (declare (xargs :stobjs (nrev state)))
  (declare (xargs :guard (string-listp filenames)))
  (let ((__function__ 'vl-read-files-aux))
    (declare (ignorable __function__))
    (b* (((when (atom filenames))
          (let ((nrev (nrev-fix nrev)))
            (mv nil nrev state)))
         ((mv okp nrev state)
          (vl-read-file-rchars (car filenames)
                               nrev))
         ((unless okp)
          (mv (msg "Error reading file ~s0."
                   (car filenames))
              nrev state)))
      (vl-read-files-aux (cdr filenames)
                         nrev))))