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