		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-tyname

Pretty-print a type name.

Signature
(pprint-tyname tn) → part
Arguments: tn — Guard (tynamep tn).
Returns: part — Type (msgp part).

If there is a declarator, we add a space beween it and the type specifier sequence. Otherwise, we just print the type specifier sequence.

Definitions and Theorems

Function: pprint-tyname

(defun pprint-tyname (tn)
  (declare (xargs :guard (tynamep tn)))
  (let ((__function__ 'pprint-tyname))
    (declare (ignorable __function__))
    (b* (((tyname tn) tn))
      (if (obj-adeclor-case tn.declor :none)
          (pprint-tyspecseq tn.tyspec)
        (msg "~@0 ~@1" (pprint-tyspecseq tn.tyspec)
             (pprint-obj-adeclor tn.declor))))))

Theorem: msgp-of-pprint-tyname

(defthm msgp-of-pprint-tyname
  (b* ((part (pprint-tyname tn)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-tyname-of-tyname-fix-tn

(defthm pprint-tyname-of-tyname-fix-tn
  (equal (pprint-tyname (tyname-fix tn))
         (pprint-tyname tn)))

Theorem: pprint-tyname-tyname-equiv-congruence-on-tn

(defthm pprint-tyname-tyname-equiv-congruence-on-tn
  (implies (tyname-equiv tn tn-equiv)
           (equal (pprint-tyname tn)
                  (pprint-tyname tn-equiv)))
  :rule-classes :congruence)