(vl-collect-ieqv-strings a x) returns all strings in the list
(vl-collect-ieqv-strings a x) → equiv-strs
This is pretty dumb, but we at least avoid downcasing
Function:
(defun vl-collect-ieqv-strings (a x) (declare (xargs :guard (and (stringp a) (string-listp x)))) (let ((__function__ 'vl-collect-ieqv-strings)) (declare (ignorable __function__)) (vl-collect-ieqv-strings-aux (str::downcase-string a) x)))
Theorem:
(defthm string-listp-of-vl-collect-ieqv-strings (implies (string-listp x) (b* ((equiv-strs (vl-collect-ieqv-strings a x))) (string-listp equiv-strs))) :rule-classes :rewrite)