		Search-engine friendly clone of the ACL2 documentation.

Vl-collect-interface-ports

Vl-collect-interface-ports-exec

Signature
(vl-collect-interface-ports-exec x nrev) → nrev
Arguments: x — Guard (vl-portlist-p x).

Definitions and Theorems

Function: vl-collect-interface-ports-exec

(defun vl-collect-interface-ports-exec (x nrev)
  (declare (xargs :stobjs (nrev)))
  (declare (xargs :guard (vl-portlist-p x)))
  (let ((__function__ 'vl-collect-interface-ports-exec))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (nrev-fix nrev))
         (x1 (vl-port-fix (car x)))
         ((when (eq (tag x1) :vl-interfaceport))
          (b* ((nrev (nrev-push x1 nrev)))
            (vl-collect-interface-ports-exec (cdr x)
                                             nrev))))
      (vl-collect-interface-ports-exec (cdr x)
                                       nrev))))

Theorem: vl-collect-interface-ports-exec-of-vl-portlist-fix-x

(defthm vl-collect-interface-ports-exec-of-vl-portlist-fix-x
  (equal (vl-collect-interface-ports-exec (vl-portlist-fix x)
                                          nrev)
         (vl-collect-interface-ports-exec x nrev)))

Theorem: vl-collect-interface-ports-exec-vl-portlist-equiv-congruence-on-x

(defthm
  vl-collect-interface-ports-exec-vl-portlist-equiv-congruence-on-x
  (implies (vl-portlist-equiv x x-equiv)
           (equal (vl-collect-interface-ports-exec x nrev)
                  (vl-collect-interface-ports-exec x-equiv nrev)))
  :rule-classes :congruence)