(vl-datatype-set-unsigned x) → new-x
Function:
(defun vl-datatype-set-unsigned (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype-set-unsigned)) (declare (ignorable __function__)) (vl-datatype-case x :vl-coretype (mbe :logic (change-vl-coretype x :signedp nil) :exec (if x.signedp (change-vl-coretype x :signedp nil) x)) :vl-struct (mbe :logic (change-vl-struct x :signedp nil) :exec (if x.signedp (change-vl-struct x :signedp nil) x)) :vl-union (mbe :logic (change-vl-union x :signedp nil) :exec (if x.signedp (change-vl-union x :signedp nil) x)) :otherwise (vl-datatype-fix x))))
Theorem:
(defthm vl-datatype-p-of-vl-datatype-set-unsigned (b* ((new-x (vl-datatype-set-unsigned x))) (vl-datatype-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-set-unsigned-of-vl-datatype-fix-x (equal (vl-datatype-set-unsigned (vl-datatype-fix x)) (vl-datatype-set-unsigned x)))
Theorem:
(defthm vl-datatype-set-unsigned-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype-set-unsigned x) (vl-datatype-set-unsigned x-equiv))) :rule-classes :congruence)