		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-coordinate

Pretty-print a group literal coordinate.

Signature
(pprint-coordinate coor) → part
Arguments: coor — Guard (coordinatep coor).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-coordinate

(defun pprint-coordinate (coor)
  (declare (xargs :guard (coordinatep coor)))
  (let ((__function__ 'pprint-coordinate))
    (declare (ignorable __function__))
    (coordinate-case coor
                     :explicit (pprint-integer coor.get)
                     :sign-high "+"
                     :sign-low "-"
                     :inferred "_")))

Theorem: msgp-of-pprint-coordinate

(defthm msgp-of-pprint-coordinate
  (b* ((part (pprint-coordinate coor)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-coordinate-of-coordinate-fix-coor

(defthm pprint-coordinate-of-coordinate-fix-coor
  (equal (pprint-coordinate (coordinate-fix coor))
         (pprint-coordinate coor)))

Theorem: pprint-coordinate-coordinate-equiv-congruence-on-coor

(defthm pprint-coordinate-coordinate-equiv-congruence-on-coor
  (implies (coordinate-equiv coor coor-equiv)
           (equal (pprint-coordinate coor)
                  (pprint-coordinate coor-equiv)))
  :rule-classes :congruence)