		Search-engine friendly clone of the ACL2 documentation.

Vl-loadconfig-clean

Vl-clean-search-extension

Normalize search extensions so that they don't have leading dots.

Signature
(vl-clean-search-extension searchext) → new-searchext
Arguments: searchext — Guard (stringp searchext).
Returns: new-searchext — Type (stringp new-searchext).

This is a DWIM feature so that we can just do the right thing regardless of whether you say the search extensions are, e.g., ".sv" or just "sv".

Definitions and Theorems

Function: vl-clean-search-extension

(defun vl-clean-search-extension (searchext)
  (declare (xargs :guard (stringp searchext)))
  (let ((__function__ 'vl-clean-search-extension))
    (declare (ignorable __function__))
    (b* ((searchext (string-fix searchext))
         (len (length searchext))
         ((when (and (< 0 len)
                     (eql (char searchext 0) #\.)))
          (subseq searchext 1 nil)))
      searchext)))

Theorem: stringp-of-vl-clean-search-extension

(defthm stringp-of-vl-clean-search-extension
  (b* ((new-searchext (vl-clean-search-extension searchext)))
    (stringp new-searchext))
  :rule-classes :type-prescription)