Function:
(defun vl-toobig-constant-atom-p (width x) (declare (xargs :guard (and (natp width) (vl-expr-p x)))) (let ((__function__ 'vl-toobig-constant-atom-p)) (declare (ignorable __function__)) (and (vl-expr-resolved-p x) (not (< (vl-resolved->val x) (ash 1 (lnfix width)))))))
Theorem:
(defthm vl-toobig-constant-atom-p-of-nfix-width (equal (vl-toobig-constant-atom-p (nfix width) x) (vl-toobig-constant-atom-p width x)))
Theorem:
(defthm vl-toobig-constant-atom-p-nat-equiv-congruence-on-width (implies (acl2::nat-equiv width width-equiv) (equal (vl-toobig-constant-atom-p width x) (vl-toobig-constant-atom-p width-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-toobig-constant-atom-p-of-vl-expr-fix-x (equal (vl-toobig-constant-atom-p width (vl-expr-fix x)) (vl-toobig-constant-atom-p width x)))
Theorem:
(defthm vl-toobig-constant-atom-p-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-toobig-constant-atom-p width x) (vl-toobig-constant-atom-p width x-equiv))) :rule-classes :congruence)