		Search-engine friendly clone of the ACL2 documentation.

Server

Vls-get-desctypes

Signature
(vls-get-desctypes data) → ans
Arguments: data — Guard (vls-data-p data).
Returns: ans — Type (stringp ans).

Definitions and Theorems

Function: vls-get-desctypes

(defun vls-get-desctypes (data)
  (declare (xargs :guard (vls-data-p data)))
  (let ((__function__ 'vls-get-desctypes))
    (declare (ignorable __function__))
    (b* ((desctypes (vl-descalist->descriptions/types
                         (vls-data->orig-descalist data))))
      (vls-success :json (bridge::json-encode desctypes)))))

Theorem: stringp-of-vls-get-desctypes

(defthm stringp-of-vls-get-desctypes
  (b* ((ans (vls-get-desctypes data)))
    (stringp ans))
  :rule-classes :type-prescription)