		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-scopestack-top-level-name

Signature
(vl-scopestack-top-level-name ss) → name
Arguments: ss — Guard (vl-scopestack-p ss).
Returns: name — Type (maybe-stringp name).

Definitions and Theorems

Function: vl-scopestack-top-level-name

(defun vl-scopestack-top-level-name (ss)
  (declare (xargs :guard (vl-scopestack-p ss)))
  (let ((__function__ 'vl-scopestack-top-level-name))
    (declare (ignorable __function__))
    (vl-scopestack-case
         ss
         :null nil
         :global nil
         :local (or (vl-scopestack-top-level-name ss.super)
                    (let ((id (vl-scope->id ss.top)))
                      (and (stringp id) id))))))

Theorem: maybe-stringp-of-vl-scopestack-top-level-name

(defthm maybe-stringp-of-vl-scopestack-top-level-name
  (b* ((name (vl-scopestack-top-level-name ss)))
    (maybe-stringp name))
  :rule-classes :type-prescription)

Theorem: vl-scopestack-top-level-name-of-vl-scopestack-fix-ss

(defthm vl-scopestack-top-level-name-of-vl-scopestack-fix-ss
  (equal (vl-scopestack-top-level-name (vl-scopestack-fix ss))
         (vl-scopestack-top-level-name ss)))

Theorem: vl-scopestack-top-level-name-vl-scopestack-equiv-congruence-on-ss

(defthm
  vl-scopestack-top-level-name-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-scopestack-top-level-name ss)
                  (vl-scopestack-top-level-name ss-equiv)))
  :rule-classes :congruence)