		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vls-describe

Signature
(vls-describe origname what data) → ans
Arguments: origname — Guard (stringp origname).; what — Guard (stringp what).; data — Guard (vls-data-p data).
Returns: ans — Type (stringp ans).

Definitions and Theorems

Function: vls-describe

(defun vls-describe (origname what data)
 (declare (xargs :guard (and (stringp origname)
                             (stringp what)
                             (vls-data-p data))))
 (let ((__function__ 'vls-describe))
  (declare (ignorable __function__))
  (b*
   (((vls-data data))
    (desc (cdr (hons-assoc-equal origname data.orig-descalist)))
    ((unless desc)
     (cat "Error: " origname " not found."))
    (ss (vl-scopestack-init data.orig))
    (blob
     (case (tag desc)
           (:vl-module (vl-module->genblob desc))
           (:vl-interface (vl-interface->genblob desc))
           (:vl-package (vl-package->genblob desc))
           (otherwise
                (make-vl-genblob :id origname
                                 :scopetype :vl-anonymous-scope)))))
   (with-local-ps (vl-ps-update-htmlp t)
                  (vl-pp-describe what blob ss)))))

Theorem: stringp-of-vls-describe

(defthm stringp-of-vls-describe
  (b* ((ans (vls-describe origname what data)))
    (stringp ans))
  :rule-classes :type-prescription)