		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vls-get-summary

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

Definitions and Theorems

Function: vls-get-summary

(defun vls-get-summary (origname data)
 (declare (xargs :guard (and (stringp origname)
                             (vls-data-p data))))
 (let ((__function__ 'vls-get-summary))
  (declare (ignorable __function__))
  (b*
   (((vls-data data))
    (desc (or (cdr (hons-assoc-equal origname data.orig-descalist))
              (vl-find-description-insensitive
                   origname data.orig-descalist)))
    ((unless desc)
     (vls-success :json (bridge::json-encode "NIL"))))
   (vls-success
       :json (bridge::json-encode (vl-description-summary desc))))))

Theorem: stringp-of-vls-get-summary

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