		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-ident

Pretty-print an identifier.

Signature
(pprint-ident id) → part
Arguments: id — Guard (identp id).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-ident

(defun pprint-ident (id)
  (declare (xargs :guard (identp id)))
  (let ((__function__ 'pprint-ident))
    (declare (ignorable __function__))
    (ident->name id)))

Theorem: msgp-of-pprint-ident

(defthm msgp-of-pprint-ident
  (b* ((part (pprint-ident id)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-ident-of-ident-fix-id

(defthm pprint-ident-of-ident-fix-id
  (equal (pprint-ident (ident-fix id))
         (pprint-ident id)))

Theorem: pprint-ident-ident-equiv-congruence-on-id

(defthm pprint-ident-ident-equiv-congruence-on-id
  (implies (ident-equiv id id-equiv)
           (equal (pprint-ident id)
                  (pprint-ident id-equiv)))
  :rule-classes :congruence)