		Search-engine friendly clone of the ACL2 documentation.

Vl-jp-atomguts

Signature
(vl-jp-atomguts x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-atomguts-p x).

Definitions and Theorems

Function: vl-jp-atomguts-fn

(defun vl-jp-atomguts-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-atomguts-p x)))
  (let ((__function__ 'vl-jp-atomguts))
    (declare (ignorable __function__))
    (case (tag x)
          (:vl-id (vl-jp-id x))
          (:vl-constint (vl-jp-constint x))
          (:vl-weirdint (vl-jp-weirdint x))
          (:vl-string (vl-jp-string x))
          (:vl-real (vl-jp-real x))
          (:vl-hidpiece (vl-jp-hidpiece x))
          (:vl-funname (vl-jp-funname x))
          (:vl-typename (vl-jp-typename x))
          (:vl-keyguts (vl-jp-keyguts x))
          (:vl-extint (vl-jp-extint x))
          (:vl-time (vl-jp-time x))
          (:vl-basictype (vl-jp-basictype x))
          (:vl-tagname (vl-jp-tagname x))
          (otherwise (vl-jp-sysfunname x)))))