		Search-engine friendly clone of the ACL2 documentation.

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)