		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))))