(vl-type-expr-pairs-sum-datatype-sizes x) → (mv warning size)
Function:
(defun vl-type-expr-pairs-sum-datatype-sizes (x) (declare (xargs :guard (vl-type-expr-pairs-p x))) (let ((__function__ 'vl-type-expr-pairs-sum-datatype-sizes)) (declare (ignorable __function__)) (b* ((x (vl-type-expr-pairs-fix x))) (if (atom x) (mv nil 0) (b* (((mv warning size1) (vl-datatype-size (caar x))) ((when warning) (mv warning nil)) ((mv warning size2) (vl-type-expr-pairs-sum-datatype-sizes (cdr x))) ((when warning) (mv warning nil))) (mv nil (+ size1 size2)))))))
Theorem:
(defthm return-type-of-vl-type-expr-pairs-sum-datatype-sizes.warning (b* (((mv common-lisp::?warning ?size) (vl-type-expr-pairs-sum-datatype-sizes x))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-type-expr-pairs-sum-datatype-sizes.size (b* (((mv common-lisp::?warning ?size) (vl-type-expr-pairs-sum-datatype-sizes x))) (implies (not warning) (natp size))) :rule-classes :type-prescription)
Theorem:
(defthm vl-type-expr-pairs-sum-datatype-sizes-of-vl-type-expr-pairs-fix-x (equal (vl-type-expr-pairs-sum-datatype-sizes (vl-type-expr-pairs-fix x)) (vl-type-expr-pairs-sum-datatype-sizes x)))
Theorem:
(defthm vl-type-expr-pairs-sum-datatype-sizes-vl-type-expr-pairs-equiv-congruence-on-x (implies (vl-type-expr-pairs-equiv x x-equiv) (equal (vl-type-expr-pairs-sum-datatype-sizes x) (vl-type-expr-pairs-sum-datatype-sizes x-equiv))) :rule-classes :congruence)