(|VL-EXPR-IS-{'0, ...}-P| x) → *
Function:
(defun |VL-EXPR-IS-{'0, ...}-P| (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ '|VL-EXPR-IS-{'0, ...}-P|)) (declare (ignorable __function__)) (vl-expr-case x :vl-concat (and (consp x.parts) (let ((first (car x.parts))) (vl-expr-case first :vl-literal (vl-value-case first.val :vl-extint (vl-bit-equiv first.val.value :vl-0val) :otherwise nil) :otherwise nil))) :otherwise nil)))
Theorem:
(defthm |VL-EXPR-IS-{'0, ...}-P-OF-VL-EXPR-FIX-X| (equal (|VL-EXPR-IS-{'0, ...}-P| (vl-expr-fix x)) (|VL-EXPR-IS-{'0, ...}-P| x)))
Theorem:
(defthm |VL-EXPR-IS-{'0, ...}-P-VL-EXPR-EQUIV-CONGRUENCE-ON-X| (implies (vl-expr-equiv x x-equiv) (equal (|VL-EXPR-IS-{'0, ...}-P| x) (|VL-EXPR-IS-{'0, ...}-P| x-equiv))) :rule-classes :congruence)