		Search-engine friendly clone of the ACL2 documentation.

Vl-scopeid

Vl-scopeid-p

Recognizer for scope names.

Signature
(vl-scopeid-p x) → bool

Definitions and Theorems

Function: vl-scopeid-p

(defun vl-scopeid-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-scopeid-p))
    (declare (ignorable __function__))
    (or (stringp x) (integerp x))))

Theorem: vl-scopeid-compound-recognizer

(defthm vl-scopeid-compound-recognizer
  (equal (vl-scopeid-p x)
         (or (stringp x) (integerp x)))
  :rule-classes :compound-recognizer)