		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-identifier

Pretty-print an identifier.

Signature
(pprint-identifier iden) → part
Arguments: iden — Guard (identifierp iden).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-identifier

(defun pprint-identifier (iden)
  (declare (xargs :guard (identifierp iden)))
  (let ((__function__ 'pprint-identifier))
    (declare (ignorable __function__))
    (identifier->name iden)))

Theorem: msgp-of-pprint-identifier

(defthm msgp-of-pprint-identifier
  (b* ((part (pprint-identifier iden)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-identifier-of-identifier-fix-iden

(defthm pprint-identifier-of-identifier-fix-iden
  (equal (pprint-identifier (identifier-fix iden))
         (pprint-identifier iden)))

Theorem: pprint-identifier-identifier-equiv-congruence-on-iden

(defthm pprint-identifier-identifier-equiv-congruence-on-iden
  (implies (identifier-equiv iden iden-equiv)
           (equal (pprint-identifier iden)
                  (pprint-identifier iden-equiv)))
  :rule-classes :congruence)