		Search-engine friendly clone of the ACL2 documentation.

Vl-scopename

Vl-scopename-p

Recognizer for scope names.

Signature
(vl-scopename-p x) → bool

Definitions and Theorems

Function: vl-scopename-p

(defun vl-scopename-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-scopename-p))
    (declare (ignorable __function__))
    (or (eq x :vl-local)
        (eq x :vl-$unit)
        (stringp x))))

Theorem: vl-scopename-p-when-stringp

(defthm vl-scopename-p-when-stringp
  (implies (stringp x)
           (vl-scopename-p x)))