• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
      • File-types
        • File-kind
        • Regular-files
        • Existing-paths
        • Missing-paths
        • Directories
        • Path-exists-p
        • Regular-file-p
        • Directory-p
        • Regular-files-p
        • Paths-all-missing-p
        • Paths-all-exist-p
        • Directories-p
        • Regular-files-exec
        • File-kind-p
        • Existing-paths-exec
        • Missing-paths-exec
        • Directories-exec
      • Argv
      • Copy
      • Catpath
      • Universal-time
      • Ls
      • Basename
      • Tempfile
      • Dirname
      • Copy!
      • Mkdir
      • Ls-files
      • Lisp-version
      • Rmtree
      • Ls-subdirs
      • Lisp-type
      • Date
      • Getpid
      • Basenames
      • Dirnames
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Basename!
      • Catpaths
      • Mkdir!
      • Ls!
      • Rmtree!
      • Remove-nonstrings
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

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