(vl-weirdint-to-concat x warnings) → (mv warnings concat)
Function:
(defun vl-weirdint-to-concat (x warnings) (declare (xargs :guard (and (vl-weirdint-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-weirdint-to-concat)) (declare (ignorable __function__)) (b* ((x (vl-weirdint-fix x)) ((vl-weirdint x) x) ((when (eq x.origtype :vl-signed)) (mv (fatal :type :vl-unsupported :msg "Don't want to think about signed weirdints, but found ~a0." :args (list x)) (make-vl-atom :guts x :finalwidth x.origwidth :finaltype :vl-signed)))) (mv (ok) (make-vl-nonatom :op :vl-concat :args (vl-weirdint-bits-to-exprs x.bits) :finalwidth x.origwidth :finaltype :vl-unsigned)))))
Theorem:
(defthm vl-warninglist-p-of-vl-weirdint-to-concat.warnings (b* (((mv ?warnings ?concat) (vl-weirdint-to-concat x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-weirdint-to-concat.concat (b* (((mv ?warnings ?concat) (vl-weirdint-to-concat x warnings))) (vl-expr-p concat)) :rule-classes :rewrite)
Theorem:
(defthm vl-weirdint-to-concat-of-vl-weirdint-fix-x (equal (vl-weirdint-to-concat (vl-weirdint-fix x) warnings) (vl-weirdint-to-concat x warnings)))
Theorem:
(defthm vl-weirdint-to-concat-vl-weirdint-equiv-congruence-on-x (implies (vl-weirdint-equiv x x-equiv) (equal (vl-weirdint-to-concat x warnings) (vl-weirdint-to-concat x-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-weirdint-to-concat-of-vl-warninglist-fix-warnings (equal (vl-weirdint-to-concat x (vl-warninglist-fix warnings)) (vl-weirdint-to-concat x warnings)))
Theorem:
(defthm vl-weirdint-to-concat-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-weirdint-to-concat x warnings) (vl-weirdint-to-concat x warnings-equiv))) :rule-classes :congruence)