(vl-udp-edge-symbol-token->interp x) → sym
Function:
(defun vl-udp-edge-symbol-token->interp (x) (declare (xargs :guard (vl-token-p x))) (declare (xargs :guard (vl-udp-edge-symbol-token-p x))) (let ((__function__ 'vl-udp-edge-symbol-token->interp)) (declare (ignorable __function__)) (case (vl-token->type x) (:vl-times :vl-udp-*) (:vl-idtoken (b* ((name (vl-idtoken->name x))) (cond ((member-equal name '("r" "R")) :vl-udp-r) ((member-equal name '("f" "F")) :vl-udp-f) ((member-equal name '("p" "P")) :vl-udp-p) ((member-equal name '("n" "N")) :vl-udp-n) (t (progn$ (impossible) :vl-udp-*))))) (otherwise (progn$ (impossible) :vl-udp-*)))))
Theorem:
(defthm vl-udpsymbol-p-of-vl-udp-edge-symbol-token->interp (b* ((sym (vl-udp-edge-symbol-token->interp x))) (vl-udpsymbol-p sym)) :rule-classes :rewrite)