		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-programid

Pretty-print a programid.

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

Definitions and Theorems

Function: pprint-programid

(defun pprint-programid (id)
  (declare (xargs :guard (programidp id)))
  (let ((__function__ 'pprint-programid))
    (declare (ignorable __function__))
    (msg "~@0.~@1"
         (pprint-identifier (programid->name id))
         (pprint-identifier (programid->network id)))))

Theorem: msgp-of-pprint-programid

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

Theorem: pprint-programid-of-programid-fix-id

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

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

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