		Search-engine friendly clone of the ACL2 documentation.

Vl-loadconfig-clean

Vl-clean-search-extensions

Signature
(vl-clean-search-extensions search-exts) → search-exts
Arguments: search-exts — Guard (string-listp search-exts).
Returns: search-exts — Type (string-listp search-exts).

Definitions and Theorems

Function: vl-clean-search-extensions

(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: string-listp-of-vl-clean-search-extensions

(defthm string-listp-of-vl-clean-search-extensions
  (b* ((search-exts (vl-clean-search-extensions search-exts)))
    (string-listp search-exts))
  :rule-classes :rewrite)