Does a path exist? After following symlinks, does it refer to any "file" at all (a regular file, a directory, a device, ...)?
(path-exists-p path &key (state 'state)) → (mv err ans new-state)
Note that we return
(defun path-exists-p-fn (path state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp path))) (let ((__function__ 'path-exists-p)) (declare (ignorable __function__)) (b* (((mv err ans state) (file-kind path)) ((when err) (mv err nil state)) (exists-p (and (not (null ans)) (not (eq ans :broken-symbolic-link))))) (mv err exists-p state))))
(defthm booleanp-of-path-exists-p.ans (b* (((mv ?err ?ans ?new-state) (path-exists-p-fn path state))) (booleanp ans)) :rule-classes :type-prescription)
(defthm state-p1-of-path-exists-p.new-state (implies (force (state-p1 state)) (b* (((mv ?err ?ans ?new-state) (path-exists-p-fn path state))) (state-p1 new-state))) :rule-classes :rewrite)