Convert the directory listing into a list of tnames.
(vl-scan-for-tnames-in-base-aux base models) → tnames
Function:
(defun vl-scan-for-tnames-in-base-aux (base models) (declare (xargs :guard (and (stringp base) (string-listp models)))) (let ((__function__ 'vl-scan-for-tnames-in-base-aux)) (declare (ignorable __function__)) (if (atom models) nil (cons (make-vl-tname :base base :model (car models)) (vl-scan-for-tnames-in-base-aux base (cdr models))))))
Theorem:
(defthm vl-tnamelist-p-of-vl-scan-for-tnames-in-base-aux (b* ((tnames (vl-scan-for-tnames-in-base-aux base models))) (vl-tnamelist-p tnames)) :rule-classes :rewrite)