		Search-engine friendly clone of the ACL2 documentation.

File-types

Missing-paths-exec

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

Definitions and Theorems

Function: missing-paths-exec-fn

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