		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-address

Pretty-print an address.

Signature
(pprint-address addr) → part
Arguments: addr — Guard (addressp addr).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-address

(defun pprint-address (addr)
  (declare (xargs :guard (addressp addr)))
  (let ((__function__ 'pprint-address))
    (declare (ignorable __function__))
    (address->name addr)))

Theorem: msgp-of-pprint-address

(defthm msgp-of-pprint-address
  (b* ((part (pprint-address addr)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-address-of-address-fix-addr

(defthm pprint-address-of-address-fix-addr
  (equal (pprint-address (address-fix addr))
         (pprint-address addr)))

Theorem: pprint-address-address-equiv-congruence-on-addr

(defthm pprint-address-address-equiv-congruence-on-addr
  (implies (address-equiv addr addr-equiv)
           (equal (pprint-address addr)
                  (pprint-address addr-equiv)))
  :rule-classes :congruence)