(vl-atomicstmt-cblock-rvalexprs x) → exprs
Function:
(defun vl-atomicstmt-cblock-rvalexprs (x) (declare (xargs :guard (and (vl-stmt-p x) (vl-atomicstmt-p x) (vl-atomicstmt-cblock-p x)))) (let ((__function__ 'vl-atomicstmt-cblock-rvalexprs)) (declare (ignorable __function__)) (case (vl-stmt-kind x) (:vl-nullstmt nil) (:vl-assignstmt (list (vl-assignstmt->expr x))) (otherwise nil))))
Theorem:
(defthm vl-exprlist-p-of-vl-atomicstmt-cblock-rvalexprs (implies (and (force (vl-stmt-p x)) (force (vl-atomicstmt-p x)) (force (vl-atomicstmt-cblock-p x))) (b* ((exprs (vl-atomicstmt-cblock-rvalexprs x))) (vl-exprlist-p exprs))) :rule-classes :rewrite)