		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vl-descalist->descriptions/types

Signature
(vl-descalist->descriptions/types x) → *
Arguments: x — Guard (vl-descalist-p x).

Definitions and Theorems

Function: vl-descalist->descriptions/types

(defun vl-descalist->descriptions/types (x)
  (declare (xargs :guard (vl-descalist-p x)))
  (let ((__function__ 'vl-descalist->descriptions/types))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((cons name description) (car x)))
      (cons (cons name (tag description))
            (vl-descalist->descriptions/types (cdr x))))))