		Search-engine friendly clone of the ACL2 documentation.

File-layout

Vl-tnames-for-base

Signature
(vl-tnames-for-base base x) → tnames
Arguments: base — Guard (stringp base).; x — Guard (vl-tnamelist-p x).
Returns: tnames — Type (vl-tnamelist-p tnames).

Definitions and Theorems

Function: vl-tnames-for-base

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

Theorem: vl-tnamelist-p-of-vl-tnames-for-base

(defthm vl-tnamelist-p-of-vl-tnames-for-base
  (b* ((tnames (vl-tnames-for-base base x)))
    (vl-tnamelist-p tnames))
  :rule-classes :rewrite)