		Search-engine friendly clone of the ACL2 documentation.

File-types

Paths-all-missing-p

Do none of these paths exist?

Signature
(paths-all-missing-p paths &key (state 'state)) → (mv err ans new-state)
Arguments: paths — Guard (string-listp paths).
Returns: err — NIL on success, or an error msg on failure.; ans — Meaningful only when there is no error.
Type (booleanp ans).; new-state — Type (state-p1 new-state), given (force (state-p1 state)).

Definitions and Theorems

Function: paths-all-missing-p-fn

(defun paths-all-missing-p-fn (paths state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (string-listp paths)))
       (let ((__function__ 'paths-all-missing-p))
            (declare (ignorable __function__))
            (b* (((when (atom paths)) (mv nil t state))
                 ((mv err ans1 state)
                  (path-exists-p (car paths)))
                 ((when err) (mv err nil state))
                 ((when ans1) (mv nil nil state)))
                (paths-all-missing-p (cdr paths)))))

Theorem: booleanp-of-paths-all-missing-p.ans

(defthm booleanp-of-paths-all-missing-p.ans
        (b* (((mv ?err ?ans ?new-state)
              (paths-all-missing-p-fn paths state)))
            (booleanp ans))
        :rule-classes :type-prescription)

Theorem: state-p1-of-paths-all-missing-p.new-state

(defthm state-p1-of-paths-all-missing-p.new-state
        (implies (force (state-p1 state))
                 (b* (((mv ?err ?ans ?new-state)
                       (paths-all-missing-p-fn paths state)))
                     (state-p1 new-state)))
        :rule-classes :rewrite)

Theorem: w-state-of-paths-all-missing-p

(defthm w-state-of-paths-all-missing-p
        (b* (((mv ?err ?ans ?new-state)
              (paths-all-missing-p-fn paths state)))
            (equal (w new-state) (w state))))