		Search-engine friendly clone of the ACL2 documentation.

Server

Vls-get-parents

Signature
(vls-get-parents 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-parents

(defun vls-get-parents (origname data)
  (declare (xargs :guard (and (stringp origname)
                              (vls-data-p data))))
  (let ((__function__ 'vls-get-parents))
    (declare (ignorable __function__))
    (b* (((vls-data data))
         (parents (vl-dependent-elements-direct (list origname)
                                                data.orig)))
      (vls-success :json (bridge::json-encode parents)))))

Theorem: stringp-of-vls-get-parents

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