		Search-engine friendly clone of the ACL2 documentation.

File-types

File-kind-p

Possible return values from file-kind.

Here nil indicates that the file does not exist.

This is an ordinary defenum.

Function: file-kind-p

(defun file-kind-p (x)
  (declare (xargs :guard t))
  (or (eq x 'nil)
      (eq x ':regular-file)
      (eq x ':directory)
      (eq x ':symbolic-link)
      (eq x ':broken-symbolic-link)
      (eq x ':pipe)
      (eq x ':socket)
      (eq x ':character-device)
      (eq x ':block-device)))

Theorem: type-when-file-kind-p

(defthm type-when-file-kind-p
  (implies (file-kind-p x)
           (if (if (symbolp x)
                   (if (not (equal x 't))
                       (not (equal x 'nil))
                     'nil)
                 'nil)
               't
             (equal x 'nil)))
  :rule-classes :compound-recognizer)