(vl-datatype->all-dims x) → dims
Function:
(defun vl-datatype->all-dims (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype->all-dims)) (declare (ignorable __function__)) (append-without-guard (vl-datatype->udims x) (vl-datatype->pdims x))))
Theorem:
(defthm vl-dimensionlist-p-of-vl-datatype->all-dims (b* ((dims (vl-datatype->all-dims x))) (vl-dimensionlist-p dims)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype->all-dims-of-vl-datatype-fix-x (equal (vl-datatype->all-dims (vl-datatype-fix x)) (vl-datatype->all-dims x)))
Theorem:
(defthm vl-datatype->all-dims-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype->all-dims x) (vl-datatype->all-dims x-equiv))) :rule-classes :congruence)