		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt-allexprs

Theorem: return-type-of-vl-stmt-allexprs.exprs

(defthm return-type-of-vl-stmt-allexprs.exprs
  (b* ((?exprs (vl-stmt-allexprs x)))
    (vl-exprlist-p exprs))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-stmtlist-allexprs.exprs

(defthm return-type-of-vl-stmtlist-allexprs.exprs
  (b* ((?exprs (vl-stmtlist-allexprs x)))
    (vl-exprlist-p exprs))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-caselist-allexprs.exprs

(defthm return-type-of-vl-caselist-allexprs.exprs
  (b* ((?exprs (vl-caselist-allexprs x)))
    (vl-exprlist-p exprs))
  :rule-classes :rewrite)

Theorem: vl-stmt-allexprs-nrev-removal

(defthm vl-stmt-allexprs-nrev-removal
  (equal (vl-stmt-allexprs-nrev x nrev)
         (append nrev (vl-stmt-allexprs x))))

Theorem: vl-stmtlist-allexprs-nrev-removal

(defthm vl-stmtlist-allexprs-nrev-removal
  (equal (vl-stmtlist-allexprs-nrev x nrev)
         (append nrev (vl-stmtlist-allexprs x))))

Theorem: vl-caselist-allexprs-nrev-removal

(defthm vl-caselist-allexprs-nrev-removal
  (equal (vl-caselist-allexprs-nrev x nrev)
         (append nrev (vl-caselist-allexprs x))))