(vl-expr-is-{n{0}}-p x) → *
Function:
(defun vl-expr-is-{n{0}}-p (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-expr-is-{n{0}}-p)) (declare (ignorable __function__)) (vl-expr-case x :vl-multiconcat (and (equal (len x.parts) 1) (let ((first (car x.parts))) (vl-expr-case first :vl-literal (vl-value-case first.val :vl-constint (equal first.val.value 0) :vl-extint (vl-bit-equiv first.val.value :vl-0val) :otherwise nil) :otherwise nil))) :otherwise nil)))
Theorem:
(defthm vl-expr-is-{n{0}}-p-of-vl-expr-fix-x (equal (vl-expr-is-{n{0}}-p (vl-expr-fix x)) (vl-expr-is-{n{0}}-p x)))
Theorem:
(defthm vl-expr-is-{n{0}}-p-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-is-{n{0}}-p x) (vl-expr-is-{n{0}}-p x-equiv))) :rule-classes :congruence)