• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
          • File-types
          • Argv
          • Copy
          • Catpath
          • Ls
          • Universal-time
          • Tempfile
          • Basename
          • Dirname
          • Copy!
          • Ls-files
          • Mkdir
          • Rmtree
          • Lisp-version
          • Lisp-type
          • Ls-subdirs
          • Date
          • Getpid
          • Dirnames
          • Basenames
          • Basename!
          • Ls-subdirs!
          • Ls-files!
          • Dirname!
          • Ls!
          • Catpaths
          • Mkdir!
          • Rmtree!
          • Remove-nonstrings
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
          • File-types
          • Argv
          • Copy
          • Catpath
          • Ls
          • Universal-time
          • Tempfile
          • Basename
          • Dirname
          • Copy!
          • Ls-files
          • Mkdir
          • Rmtree
          • Lisp-version
          • Lisp-type
          • Ls-subdirs
          • Date
          • Getpid
          • Dirnames
          • Basenames
          • Basename!
          • Ls-subdirs!
          • Ls-files!
          • Dirname!
          • Ls!
          • Catpaths
          • Mkdir!
          • Rmtree!
          • Remove-nonstrings
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Oslib

      Remove-nonstrings

      Signature
      (remove-nonstrings x) → filtered-x
      Returns
      filtered-x — Type (string-listp filtered-x).

      Definitions and Theorems

      Function: remove-nonstrings

      (defun remove-nonstrings (x)
        (declare (xargs :guard t))
        (let ((__function__ 'remove-nonstrings))
          (declare (ignorable __function__))
          (cond ((atom x) nil)
                ((stringp (car x))
                 (cons (car x)
                       (remove-nonstrings (cdr x))))
                (t (remove-nonstrings (cdr x))))))

      Theorem: string-listp-of-remove-nonstrings

      (defthm string-listp-of-remove-nonstrings
        (b* ((filtered-x (remove-nonstrings x)))
          (string-listp filtered-x))
        :rule-classes :rewrite)