		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Evisceratedp

Signature
(evisceratedp x) → *

Definitions and Theorems

Function: evisceratedp$inline

(defun evisceratedp$inline (x)
  (declare (xargs :guard (consp x)))
  (let ((acl2::__function__ 'evisceratedp))
    (declare (ignorable acl2::__function__))
    (and (eq (car x) :evisceration-mark)
         (stringp (cdr x)))))