		Search-engine friendly clone of the ACL2 documentation.

Vl-server

Vl-ppc-description

Signature
(vl-ppc-description x ss &key (ps 'ps)) → ps
Arguments: x — Guard (vl-description-p x).; ss — Guard (vl-scopestack-p ss).

Definitions and Theorems

Function: vl-ppc-description-fn

(defun vl-ppc-description-fn (x ss ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (and (vl-description-p x)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-ppc-description))
    (declare (ignorable __function__))
    (b* ((x (vl-description-fix x)))
      (case (tag x)
            (:vl-module (vl-ppc-module x ss))
            (:vl-udp (vl-ppc-udp x))
            (:vl-interface (vl-ppc-interface x ss))
            (:vl-package (vl-ppc-package x ss))
            (:vl-program (vl-ppc-program x))
            (:vl-class (vl-ppc-class x))
            (:vl-config (vl-ppc-config x))
            (:vl-taskdecl (vl-pp-taskdecl x))
            (:vl-fundecl (vl-pp-fundecl x))
            (:vl-paramdecl (vl-pp-paramdecl x))
            (:vl-import (vl-pp-import x))
            (:vl-fwdtypedef (vl-pp-fwdtypedef x))
            (:vl-vardecl (vl-pp-vardecl x))
            (:vl-dpiimport (vl-pp-dpiimport x))
            (:vl-dpiexport (vl-pp-dpiexport x))
            (:vl-bind (vl-pp-bind x ss))
            (:vl-property (vl-pp-property x))
            (:vl-sequence (vl-pp-sequence x))
            (otherwise (vl-pp-typedef x))))))