		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)