Build lists of vl-emodwire-ps for a vl-plainarglist-p.
(vl-plainarglist-lsb-pattern x walist warnings) → (mv successp warnings pattern)
We project vl-plainarg-lsb-bits across a list of arguments, and cons together the resulting bits to produce an vl-emodwirelistlist-p where each sub-list is in LSB-order.
Function:
(defun vl-plainarglist-lsb-pattern (x walist warnings) (declare (xargs :guard (and (vl-plainarglist-p x) (vl-wirealist-p walist) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-plainarglist-lsb-pattern)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil)) ((mv car-successp warnings car-lsb-bits) (vl-plainarg-lsb-bits (car x) walist warnings)) ((mv cdr-successp warnings cdr-lsb-pattern) (vl-plainarglist-lsb-pattern (cdr x) walist warnings))) (mv (and car-successp cdr-successp) warnings (cons car-lsb-bits cdr-lsb-pattern)))))
Theorem:
(defthm booleanp-of-vl-plainarglist-lsb-pattern.successp (b* (((mv ?successp ?warnings ?pattern) (vl-plainarglist-lsb-pattern x walist warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-plainarglist-lsb-pattern.warnings (b* (((mv ?successp ?warnings ?pattern) (vl-plainarglist-lsb-pattern x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-emodwirelistlist-p-of-vl-plainarglist-lsb-pattern.pattern (b* (((mv ?successp ?warnings ?pattern) (vl-plainarglist-lsb-pattern x walist warnings))) (vl-emodwirelistlist-p pattern)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-plainarglist-lsb-pattern.pattern (b* (((mv ?successp ?warnings ?pattern) (vl-plainarglist-lsb-pattern x walist warnings))) (true-listp pattern)) :rule-classes :type-prescription)
Theorem:
(defthm true-list-listp-of-vl-plainarglist-lsb-pattern.pattern (b* (((mv ?successp ?warnings ?pattern) (vl-plainarglist-lsb-pattern x walist warnings))) (true-list-listp pattern)) :rule-classes :rewrite)