		Search-engine friendly clone of the ACL2 documentation.

Vl-emodwire-p

Vl-emodwire->basename

Returns the name of an vl-emodwire-p, excluding the index, as a string.

For instance, the basename of |opcode[3]| is "opcode", and the basename of |reset| is "reset".

Definitions and Theorems

Function: vl-emodwire->basename

(defun vl-emodwire->basename (x)
  (declare (xargs :guard (vl-emodwire-p x)))
  (b* ((name (symbol-name x))
       (open (position #\[ name)))
    (vl-emodwire-decode (if open (subseq name 0 open) name))))

Theorem: stringp-of-vl-emodwire->basename

(defthm stringp-of-vl-emodwire->basename
  (stringp (vl-emodwire->basename x))
  :rule-classes :type-prescription)

Theorem: vl-emodwire->basename-of-vl-emodwire

(defthm vl-emodwire->basename-of-vl-emodwire
  (implies
       (and (force (stringp basename))
            (force (maybe-natp index)))
       (equal (vl-emodwire->basename (vl-emodwire basename index))
              basename)))