(vl-assign-can-skip-trunc-p x) → *
Function:
(defun vl-assign-can-skip-trunc-p$inline (x) (declare (xargs :guard (vl-assign-p x))) (let ((__function__ 'vl-assign-can-skip-trunc-p)) (declare (ignorable __function__)) (b* ((lhsw (vl-expr->finalwidth (vl-assign->lvalue x))) (rhsw (vl-expr->finalwidth (vl-assign->expr x)))) (and lhsw (eql lhsw rhsw)))))
Theorem:
(defthm vl-assign-can-skip-trunc-p$inline-of-vl-assign-fix-x (equal (vl-assign-can-skip-trunc-p$inline (vl-assign-fix x)) (vl-assign-can-skip-trunc-p$inline x)))
Theorem:
(defthm vl-assign-can-skip-trunc-p$inline-vl-assign-equiv-congruence-on-x (implies (vl-assign-equiv x x-equiv) (equal (vl-assign-can-skip-trunc-p$inline x) (vl-assign-can-skip-trunc-p$inline x-equiv))) :rule-classes :congruence)