(vl-udp-level-symbol-token->interp x) → level
Function:
(defun vl-udp-level-symbol-token->interp (x) (declare (xargs :guard (vl-token-p x))) (declare (xargs :guard (vl-udp-level-symbol-token-p x))) (let ((__function__ 'vl-udp-level-symbol-token->interp)) (declare (ignorable __function__)) (case (vl-token->type x) (:vl-inttoken (case (vl-echar->char (car (vl-inttoken->etext x))) (#\0 :vl-udp-0) (#\1 :vl-udp-1) (otherwise (progn$ (impossible) :vl-udp-0)))) (:vl-idtoken (let ((name (vl-idtoken->name x))) (cond ((member-equal name '("x" "X")) :vl-udp-x) ((member-equal name '("b" "B")) :vl-udp-b) (t (progn$ (impossible) :vl-udp-0))))) (:vl-qmark :vl-udp-?) (otherwise (progn$ (impossible) :vl-udp-0)))))
Theorem:
(defthm vl-udpsymbol-p-of-vl-udp-level-symbol-token->interp (b* ((level (vl-udp-level-symbol-token->interp x))) (vl-udpsymbol-p level)) :rule-classes :rewrite)