		Search-engine friendly clone of the ACL2 documentation.

File-types

Directories-exec

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

Definitions and Theorems

Function: directories-exec-fn

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