		Search-engine friendly clone of the ACL2 documentation.

File-layout

Vl-tnames-to-json-aux

Signature
(vl-tnames-to-json-aux bases x) → *
Arguments: bases — Guard (string-listp bases).; x — Guard (vl-tnamelist-p x).

Definitions and Theorems

Function: vl-tnames-to-json-aux

(defun vl-tnames-to-json-aux (bases x)
  (declare (xargs :guard (and (string-listp bases)
                              (vl-tnamelist-p x))))
  (let ((__function__ 'vl-tnames-to-json-aux))
    (declare (ignorable __function__))
    (b* (((when (atom bases)) nil)
         (base1 (car bases))
         (tnames1 (vl-tnames-for-base base1 x))
         (models1 (vl-tnamelist-models tnames1)))
      (cons (cons base1 models1)
            (vl-tnames-to-json-aux (cdr bases)
                                   x)))))