		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))))))