		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-remove-null-statements

Signature
(vl-remove-null-statements x) → new-x
Arguments: x — Guard (vl-stmtlist-p x).
Returns: new-x — Type (vl-stmtlist-p new-x), given the guard.

Definitions and Theorems

Function: vl-remove-null-statements

(defun vl-remove-null-statements (x)
  (declare (xargs :guard (vl-stmtlist-p x)))
  (let ((__function__ 'vl-remove-null-statements))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((vl-nullstmt-p (car x))
           (vl-remove-null-statements (cdr x)))
          (t (cons (car x)
                   (vl-remove-null-statements (cdr x)))))))

Theorem: vl-stmtlist-p-of-vl-remove-null-statements

(defthm vl-stmtlist-p-of-vl-remove-null-statements
  (implies (and (force (vl-stmtlist-p x)))
           (b* ((new-x (vl-remove-null-statements x)))
             (vl-stmtlist-p new-x)))
  :rule-classes :rewrite)