		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Eviscerated->guts

Signature
(eviscerated->guts x) → guts
Arguments: x — Guard (and (consp x) (evisceratedp x)).
Returns: guts — Type (stringp guts).

Definitions and Theorems

Function: eviscerated->guts$inline

(defun eviscerated->guts$inline (x)
  (declare (xargs :guard (and (consp x) (evisceratedp x))))
  (let ((acl2::__function__ 'eviscerated->guts))
    (declare (ignorable acl2::__function__))
    (mbe :logic (str-fix (cdr x))
         :exec (cdr x))))

Theorem: stringp-of-eviscerated->guts

(defthm stringp-of-eviscerated->guts
  (b* ((guts (eviscerated->guts$inline x)))
    (stringp guts))
  :rule-classes :type-prescription)