Gather all top-level expressions from a vl-paramtype-p.
(vl-paramtype-allexprs x) → exprs
Function:
(defun vl-paramtype-allexprs (x) (declare (xargs :guard (vl-paramtype-p x))) (let ((__function__ 'vl-paramtype-allexprs)) (declare (ignorable __function__)) (mbe :logic (b* ((x (vl-paramtype-fix x))) (vl-paramtype-case x (:vl-implicitvalueparam (append (vl-maybe-range-allexprs x.range) (vl-maybe-expr-allexprs x.default))) (:vl-explicitvalueparam (append (vl-datatype-allexprs x.type) (vl-maybe-expr-allexprs x.default))) (:vl-typeparam (vl-maybe-datatype-allexprs x.default)))) :exec (with-local-nrev (vl-paramtype-allexprs-nrev x nrev)))))
Theorem:
(defthm vl-exprlist-p-of-vl-paramtype-allexprs (b* ((exprs (vl-paramtype-allexprs x))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-paramtype-allexprs (true-listp (vl-paramtype-allexprs x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-paramtype-allexprs-nrev-removal (equal (vl-paramtype-allexprs-nrev x nrev) (append nrev (vl-paramtype-allexprs x))))
Theorem:
(defthm vl-paramtype-allexprs-of-vl-paramtype-fix-x (equal (vl-paramtype-allexprs (vl-paramtype-fix x)) (vl-paramtype-allexprs x)))
Theorem:
(defthm vl-paramtype-allexprs-vl-paramtype-equiv-congruence-on-x (implies (vl-paramtype-equiv x x-equiv) (equal (vl-paramtype-allexprs x) (vl-paramtype-allexprs x-equiv))) :rule-classes :congruence)