		Search-engine friendly clone of the ACL2 documentation.

Server

Vls-get-children

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

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

Theorem: stringp-of-vls-get-children

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