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))
(:vl-package (vl-ppc-package x))
(:vl-program (vl-ppc-program 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))
(otherwise (vl-pp-typedef x))))))
