		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-idscope

Signature
(vl-idscope name) → scopeexpr
Arguments: name — Guard (stringp name).
Returns: scopeexpr — Type (vl-scopeexpr-p scopeexpr).

Definitions and Theorems

Function: vl-idscope

(defun vl-idscope (name)
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'vl-idscope))
    (declare (ignorable __function__))
    (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name name))))

Theorem: vl-scopeexpr-p-of-vl-idscope

(defthm vl-scopeexpr-p-of-vl-idscope
  (b* ((scopeexpr (vl-idscope name)))
    (vl-scopeexpr-p scopeexpr))
  :rule-classes :rewrite)

Theorem: vl-idscope-p-of-vl-idscope

(defthm vl-idscope-p-of-vl-idscope
  (b* ((?scopeexpr (vl-idscope name)))
    (vl-idscope-p scopeexpr)))

Theorem: vl-idscope->name-of-vl-idscope

(defthm vl-idscope->name-of-vl-idscope
  (b* ((?scopeexpr (vl-idscope name)))
    (equal (vl-idscope->name scopeexpr)
           (string-fix name))))

Theorem: vl-idscope-of-str-fix-name

(defthm vl-idscope-of-str-fix-name
  (equal (vl-idscope (str-fix name))
         (vl-idscope name)))

Theorem: vl-idscope-streqv-congruence-on-name

(defthm vl-idscope-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-idscope name)
                  (vl-idscope name-equiv)))
  :rule-classes :congruence)