		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-locator

Pretty-print a locator.

Signature
(pprint-locator loc) → part
Arguments: loc — Guard (locatorp loc).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-locator

(defun pprint-locator (loc)
  (declare (xargs :guard (locatorp loc)))
  (let ((__function__ 'pprint-locator))
    (declare (ignorable __function__))
    (msg "~@0/~@1"
         (pprint-programid (locator->program loc))
         (pprint-identifier (locator->name loc)))))

Theorem: msgp-of-pprint-locator

(defthm msgp-of-pprint-locator
  (b* ((part (pprint-locator loc)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-locator-of-locator-fix-loc

(defthm pprint-locator-of-locator-fix-loc
  (equal (pprint-locator (locator-fix loc))
         (pprint-locator loc)))

Theorem: pprint-locator-locator-equiv-congruence-on-loc

(defthm pprint-locator-locator-equiv-congruence-on-loc
  (implies (locator-equiv loc loc-equiv)
           (equal (pprint-locator loc)
                  (pprint-locator loc-equiv)))
  :rule-classes :congruence)