		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-label

Pretty-print a label.

Signature
(pprint-label lab) → part
Arguments: lab — Guard (labelp lab).
Returns: part — Type (msgp part).

We also print a space just after the colon, so that the sub-statement after the label is separated by a space.

Definitions and Theorems

Function: pprint-label

(defun pprint-label (lab)
  (declare (xargs :guard (labelp lab)))
  (let ((__function__ 'pprint-label))
    (declare (ignorable __function__))
    (label-case lab
                :name (msg "~@0: " (pprint-ident lab.get))
                :cas "case: "
                :default "default: ")))

Theorem: msgp-of-pprint-label

(defthm msgp-of-pprint-label
  (b* ((part (pprint-label lab)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-label-of-label-fix-lab

(defthm pprint-label-of-label-fix-lab
  (equal (pprint-label (label-fix lab))
         (pprint-label lab)))

Theorem: pprint-label-label-equiv-congruence-on-lab

(defthm pprint-label-label-equiv-congruence-on-lab
  (implies (label-equiv lab lab-equiv)
           (equal (pprint-label lab)
                  (pprint-label lab-equiv)))
  :rule-classes :congruence)