(vl-clean-search-extensions search-exts) → search-exts
Function:
(defun vl-clean-search-extensions (search-exts) (declare (xargs :guard (string-listp search-exts))) (let ((__function__ 'vl-clean-search-extensions)) (declare (ignorable __function__)) (remove-duplicates-equal (remove-equal "" (vl-clean-search-extensions-aux search-exts)))))
Theorem:
(defthm string-listp-of-vl-clean-search-extensions (b* ((search-exts (vl-clean-search-extensions search-exts))) (string-listp search-exts)) :rule-classes :rewrite)