(vl-interpret-dpi-spec-token x) → spec
Function:
(defun vl-interpret-dpi-spec-token (x) (declare (xargs :guard (vl-token-p x))) (declare (xargs :guard (vl-dpi-spec-token-p x))) (let ((__function__ 'vl-interpret-dpi-spec-token)) (declare (ignorable __function__)) (b* ((expansion (vl-stringtoken->expansion x))) (cond ((equal expansion "DPI") :vl-dpi) ((equal expansion "DPI-C") :vl-dpi-c) (t (progn$ (impossible) :vl-dpi))))))
Theorem:
(defthm vl-dpispec-p-of-vl-interpret-dpi-spec-token (b* ((spec (vl-interpret-dpi-spec-token x))) (vl-dpispec-p spec)) :rule-classes :rewrite)