		Search-engine friendly clone of the ACL2 documentation.

Esim-vl-iopattern-p

Esim-vl-iopattern-entry->basename

(esim-vl-iopattern-entry->basename x) returns the basename that is shared by all the members of a esim-vl-iopattern-entry-p.

For instance, it returns "A" for (A[0] A[1] ... A[N]).

Definitions and Theorems

Function: esim-vl-iopattern-entry->basename

(defun esim-vl-iopattern-entry->basename (x)
  (declare (xargs :guard (esim-vl-iopattern-entry-p x)))
  (mbe :logic (string-fix (vl-emodwire->basename (car x)))
       :exec (vl-emodwire->basename (car x))))

Theorem: stringp-of-esim-vl-iopattern-entry->basename

(defthm stringp-of-esim-vl-iopattern-entry->basename
  (stringp (esim-vl-iopattern-entry->basename x))
  :rule-classes :type-prescription)