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