		Search-engine friendly clone of the ACL2 documentation.

Cblock

Vl-stmt-cblock-lvalexprs

Collect expressions used in left-hand side positions.

Signature
(vl-stmt-cblock-lvalexprs x) → exprs
Arguments: x — Guard (and (vl-stmt-p x) (vl-stmt-cblock-p x)).
Returns: exprs — Type (and (vl-exprlist-p exprs) (vl-idexprlist-p exprs)), given the guard.

Theorem: return-type-of-vl-stmt-cblock-lvalexprs.exprs

(defthm return-type-of-vl-stmt-cblock-lvalexprs.exprs
  (implies (and (force (vl-stmt-p x))
                (force (vl-stmt-cblock-p x)))
           (b* ((?exprs (vl-stmt-cblock-lvalexprs x)))
             (and (vl-exprlist-p exprs)
                  (vl-idexprlist-p exprs))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-stmtlist-cblock-lvalexprs.exprs

(defthm return-type-of-vl-stmtlist-cblock-lvalexprs.exprs
  (implies (and (force (vl-stmtlist-p x))
                (force (vl-stmtlist-cblock-p x)))
           (b* ((?exprs (vl-stmtlist-cblock-lvalexprs x)))
             (and (vl-exprlist-p exprs)
                  (vl-idexprlist-p exprs))))
  :rule-classes :rewrite)

Subtopics

Vl-atomicstmt-cblock-lvalexprs
Vl-stmtlist-cblock-lvalexprs