		Search-engine friendly clone of the ACL2 documentation.

File-types

Regular-files-exec

Signature
(regular-files-exec paths acc &key (state 'state)) → (mv * * state)
Arguments: paths — Guard (string-listp paths).

Definitions and Theorems

Function: regular-files-exec-fn

(defun regular-files-exec-fn (paths acc state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (string-listp paths)))
  "Tail recursive version for execution."
  (let ((__function__ 'regular-files-exec))
    (declare (ignorable __function__))
    (b* (((when (atom paths)) (mv nil acc state))
         ((mv err regular-p state)
          (regular-file-p (car paths)))
         ((when err) (mv err acc state))
         (acc (if regular-p (cons (car paths) acc)
                acc)))
      (regular-files-exec (cdr paths) acc))))