(vl-datatype-allexprs x) → exprs
Theorem:
(defthm return-type-of-vl-datatype-allexprs.exprs (b* ((?exprs (vl-datatype-allexprs x))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-structmemberlist-allexprs.exprs (b* ((?exprs (vl-structmemberlist-allexprs x))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-structmember-allexprs.exprs (b* ((?exprs (vl-structmember-allexprs x))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-allexprs-nrev-removal (equal (vl-datatype-allexprs-nrev x nrev) (append nrev (vl-datatype-allexprs x))))
Theorem:
(defthm vl-structmemberlist-allexprs-nrev-removal (equal (vl-structmemberlist-allexprs-nrev x nrev) (append nrev (vl-structmemberlist-allexprs x))))
Theorem:
(defthm vl-structmember-allexprs-nrev-removal (equal (vl-structmember-allexprs-nrev x nrev) (append nrev (vl-structmember-allexprs x))))