		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-ifportexpr->name

Signature
(vl-ifportexpr->name x) → name
Arguments: x — Guard (vl-expr-p x).
Returns: name — Type (maybe-stringp name).

Definitions and Theorems

Function: vl-ifportexpr->name

(defun vl-ifportexpr->name (x)
 (declare (xargs :guard (vl-expr-p x)))
 (let ((__function__ 'vl-ifportexpr->name))
  (declare (ignorable __function__))
  (vl-expr-case
   x
   :vl-index
   (vl-scopeexpr-case
     x.scope
     :colon nil
     :end
     (vl-hidexpr-case x.scope.hid :dot
                      (b* (((vl-hidindex x.scope.hid.first)))
                        (and (atom x.scope.hid.first.indices)
                             (vl-hidexpr-case x.scope.hid.rest :end)
                             (stringp x.scope.hid.first.name)
                             x.scope.hid.first.name))
                      :end x.scope.hid.name))
   :otherwise nil)))

Theorem: maybe-stringp-of-vl-ifportexpr->name

(defthm maybe-stringp-of-vl-ifportexpr->name
  (b* ((name (vl-ifportexpr->name x)))
    (maybe-stringp name))
  :rule-classes :rewrite)

Theorem: vl-ifportexpr->name-of-vl-expr-fix-x

(defthm vl-ifportexpr->name-of-vl-expr-fix-x
  (equal (vl-ifportexpr->name (vl-expr-fix x))
         (vl-ifportexpr->name x)))

Theorem: vl-ifportexpr->name-vl-expr-equiv-congruence-on-x

(defthm vl-ifportexpr->name-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-ifportexpr->name x)
                  (vl-ifportexpr->name x-equiv)))
  :rule-classes :congruence)