		Search-engine friendly clone of the ACL2 documentation.

Esim-vl-iopattern-p

All-equalp-of-vl-emodwirelist->basenames

(all-equalp-of-vl-emodwirelist->basenames basename x) ensures that all of the vl-emodwire-ps in x have this basename.

Definitions and Theorems

Function: all-equalp-of-vl-emodwirelist->basenames

(defun
 all-equalp-of-vl-emodwirelist->basenames
 (basename x)
 (declare (xargs :guard (and (stringp basename)
                             (vl-emodwirelist-p x))))
 (mbe
  :logic (all-equalp basename (vl-emodwirelist->basenames x))
  :exec
  (if
   (atom x)
   t
   (and
     (equal basename
            (vl-emodwire->basename (car x)))
     (all-equalp-of-vl-emodwirelist->basenames basename (cdr x))))))