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