(vl-make-guts-from-inttoken x) → guts
Function:
(defun vl-make-guts-from-inttoken (x) (declare (xargs :guard (vl-inttoken-p x))) (let ((__function__ 'vl-make-guts-from-inttoken)) (declare (ignorable __function__)) (b* (((vl-inttoken x) x)) (if x.value (make-vl-constint :origwidth x.width :origtype (if x.signedp :vl-signed :vl-unsigned) :value x.value :wasunsized x.wasunsized) (make-vl-weirdint :origwidth x.width :origtype (if x.signedp :vl-signed :vl-unsigned) :bits x.bits :wasunsized x.wasunsized)))))
Theorem:
(defthm vl-atomguts-p-of-vl-make-guts-from-inttoken (implies (and (force (vl-inttoken-p x))) (b* ((guts (vl-make-guts-from-inttoken x))) (vl-atomguts-p guts))) :rule-classes :rewrite)