		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-evatomlist->subexprs

Signature
(vl-evatomlist->subexprs x) → subexprs
Arguments: x — Guard (vl-evatomlist-p x).
Returns: subexprs — Type (vl-exprlist-p subexprs).

Definitions and Theorems

Function: vl-evatomlist->subexprs

(defun vl-evatomlist->subexprs (x)
  (declare (xargs :guard (vl-evatomlist-p x)))
  (let ((__function__ 'vl-evatomlist->subexprs))
    (declare (ignorable __function__))
    (let ((x (vl-evatomlist-fix x)))
      (if (atom x)
          nil
        (cons (vl-evatom->expr (car x))
              (vl-evatomlist->subexprs (cdr x)))))))

Theorem: vl-exprlist-p-of-vl-evatomlist->subexprs

(defthm vl-exprlist-p-of-vl-evatomlist->subexprs
  (b* ((subexprs (vl-evatomlist->subexprs x)))
    (vl-exprlist-p subexprs))
  :rule-classes :rewrite)

Theorem: len-of-vl-evatomlist->subexprs

(defthm len-of-vl-evatomlist->subexprs
  (equal (len (vl-evatomlist->subexprs x))
         (len x)))

Theorem: vl-exprlist-count-of-vl-evatomlist->subexprs

(defthm vl-exprlist-count-of-vl-evatomlist->subexprs
  (b* ((?subexprs (vl-evatomlist->subexprs x)))
    (<= (vl-exprlist-count subexprs)
        (vl-evatomlist-count x)))
  :rule-classes :linear)

Theorem: vl-evatomlist->subexprs-of-vl-evatomlist-fix-x

(defthm vl-evatomlist->subexprs-of-vl-evatomlist-fix-x
  (equal (vl-evatomlist->subexprs (vl-evatomlist-fix x))
         (vl-evatomlist->subexprs x)))

Theorem: vl-evatomlist->subexprs-vl-evatomlist-equiv-congruence-on-x

(defthm vl-evatomlist->subexprs-vl-evatomlist-equiv-congruence-on-x
  (implies (vl-evatomlist-equiv x x-equiv)
           (equal (vl-evatomlist->subexprs x)
                  (vl-evatomlist->subexprs x-equiv)))
  :rule-classes :congruence)