		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt-unelse

Recursively processes all the if statements.

Theorem: len-of-vl-stmtlist-unelse

(defthm len-of-vl-stmtlist-unelse
  (equal (len (vl-stmtlist-unelse x))
         (len x)))

Theorem: return-type-of-vl-stmt-unelse

(defthm return-type-of-vl-stmt-unelse
  (implies (force (vl-stmt-p x))
           (vl-stmt-p (vl-stmt-unelse x))))

Theorem: return-type-of-vl-stmtlist-unelse

(defthm return-type-of-vl-stmtlist-unelse
  (implies (force (vl-stmtlist-p x))
           (vl-stmtlist-p (vl-stmtlist-unelse x))))