		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-hidexpr->subexprs

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

Definitions and Theorems

Function: vl-hidexpr->subexprs

(defun vl-hidexpr->subexprs (x)
 (declare (xargs :guard (vl-hidexpr-p x)))
 (let ((__function__ 'vl-hidexpr->subexprs))
   (declare (ignorable __function__))
   (vl-hidexpr-case
        x
        :end nil
        :dot (append-without-guard (vl-hidindex->indices x.first)
                                   (vl-hidexpr->subexprs x.rest)))))

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

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

Theorem: vl-hidexpr->subexprs-true-listp

(defthm vl-hidexpr->subexprs-true-listp
  (b* nil
    (true-listp (vl-hidexpr->subexprs x)))
  :rule-classes :type-prescription)

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

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

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

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

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

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