		Search-engine friendly clone of the ACL2 documentation.

Name

Name-p

Signature
(name-p x) → *

Definitions and Theorems

Function: name-p

(defun name-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'name-p))
    (declare (ignorable __function__))
    (or (stringp x)
        (integerp x)
        (eq x :self)
        (and (consp x)
             (eq (car x) :anonymous)))))