Get the declarations, if any, from an arbitrary compound (non-atomic) statement.
(vl-compoundstmt->paramdecls x) → decls
This really only makes sense for block statements.
Function:
(defun vl-compoundstmt->paramdecls (x) (declare (xargs :guard (vl-stmt-p x))) (declare (xargs :guard (not (vl-atomicstmt-p x)))) (let ((__function__ 'vl-compoundstmt->paramdecls)) (declare (ignorable __function__)) (vl-stmt-case x :vl-blockstmt x.paramdecls :otherwise nil)))
Theorem:
(defthm vl-paramdecllist-p-of-vl-compoundstmt->paramdecls (b* ((decls (vl-compoundstmt->paramdecls x))) (vl-paramdecllist-p decls)) :rule-classes :rewrite)
Theorem:
(defthm vl-compoundstmt->paramdecls-is-usually-nil (implies (not (vl-stmt-case x :vl-blockstmt)) (equal (vl-compoundstmt->paramdecls x) nil)))
Theorem:
(defthm vl-compoundstmt->paramdecls-of-vl-stmt-fix-x (equal (vl-compoundstmt->paramdecls (vl-stmt-fix x)) (vl-compoundstmt->paramdecls x)))
Theorem:
(defthm vl-compoundstmt->paramdecls-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-compoundstmt->paramdecls x) (vl-compoundstmt->paramdecls x-equiv))) :rule-classes :congruence)