		Search-engine friendly clone of the ACL2 documentation.

Server

Vl-find-description-insensitive

Signature
(vl-find-description-insensitive name descalist) → desc
Arguments: name — Guard (stringp name).; descalist — Guard (vl-descalist-p descalist).
Returns: desc — Type (iff (vl-description-p desc) desc).

Definitions and Theorems

Function: vl-find-description-insensitive

(defun vl-find-description-insensitive (name descalist)
  (declare (xargs :guard (and (stringp name)
                              (vl-descalist-p descalist))))
  (let ((__function__ 'vl-find-description-insensitive))
    (declare (ignorable __function__))
    (b* (((when (atom descalist)) nil)
         ((cons name1 desc1) (car descalist))
         ((when (str::istreqv name name1))
          (vl-description-fix desc1)))
      (vl-find-description-insensitive name (cdr descalist)))))

Theorem: return-type-of-vl-find-description-insensitive

(defthm return-type-of-vl-find-description-insensitive
  (b* ((desc (vl-find-description-insensitive name descalist)))
    (iff (vl-description-p desc) desc))
  :rule-classes :rewrite)