• Top

• Sv::vl-moddb.lisp

Vl-portinfolist-vars

Signature

(vl-portinfolist-vars x) → vars

Arguments

x — Guard (vl-portinfolist-p x).

Returns

vars — Type (sv::svarlist-p vars).

Definitions and Theorems

Function: vl-portinfolist-vars

(defun vl-portinfolist-vars (x)
  (declare (xargs :guard (vl-portinfolist-p x)))
  (let ((__function__ 'vl-portinfolist-vars))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (append (vl-portinfo-vars (car x))
              (vl-portinfolist-vars (cdr x))))))

Theorem: svarlist-p-of-vl-portinfolist-vars

(defthm svarlist-p-of-vl-portinfolist-vars
  (b* ((vars (vl-portinfolist-vars x)))
    (sv::svarlist-p vars))
  :rule-classes :rewrite)

Theorem: vl-portinfolist-vars-of-vl-portinfolist-fix-x

(defthm vl-portinfolist-vars-of-vl-portinfolist-fix-x
  (equal (vl-portinfolist-vars (vl-portinfolist-fix x))
         (vl-portinfolist-vars x)))

Theorem: vl-portinfolist-vars-vl-portinfolist-equiv-congruence-on-x

(defthm vl-portinfolist-vars-vl-portinfolist-equiv-congruence-on-x
  (implies (vl-portinfolist-equiv x x-equiv)
           (equal (vl-portinfolist-vars x)
                  (vl-portinfolist-vars x-equiv)))
  :rule-classes :congruence)