		Search-engine friendly clone of the ACL2 documentation.

File-layout

Vl-find-tname

Signature
(vl-find-tname base model x) → tname
Arguments: base — Guard (stringp base).; model — Guard (stringp model).; x — Guard (vl-tnamelist-p x).
Returns: tname — Type (equal (vl-tname-p tname) (if tname t nil)).

Definitions and Theorems

Function: vl-find-tname

(defun vl-find-tname (base model x)
  (declare (xargs :guard (and (stringp base)
                              (stringp model)
                              (vl-tnamelist-p x))))
  (let ((__function__ 'vl-find-tname))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((and (equal base (vl-tname->base (car x)))
                (equal model (vl-tname->model (car x))))
           (vl-tname-fix (car x)))
          (t (vl-find-tname base model (cdr x))))))

Theorem: return-type-of-vl-find-tname

(defthm return-type-of-vl-find-tname
  (b* ((tname (vl-find-tname base model x)))
    (equal (vl-tname-p tname)
           (if tname t nil)))
  :rule-classes :rewrite)