		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-type

Pretty-print a type.

Signature
(pprint-type type) → part
Arguments: type — Guard (typep type).
Returns: part — Type (msgp part).

Theorem: return-type-of-pprint-type.part

(defthm return-type-of-pprint-type.part
  (b* ((?part (pprint-type type)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: return-type-of-pprint-type-list.parts

(defthm return-type-of-pprint-type-list.parts
  (b* ((?parts (pprint-type-list types)))
    (msg-listp parts))
  :rule-classes :rewrite)

Theorem: pprint-type-of-type-fix-type

(defthm pprint-type-of-type-fix-type
  (equal (pprint-type (type-fix type))
         (pprint-type type)))

Theorem: pprint-type-list-of-type-list-fix-types

(defthm pprint-type-list-of-type-list-fix-types
  (equal (pprint-type-list (type-list-fix types))
         (pprint-type-list types)))

Theorem: pprint-type-type-equiv-congruence-on-type

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

Theorem: pprint-type-list-type-list-equiv-congruence-on-types

(defthm pprint-type-list-type-list-equiv-congruence-on-types
  (implies (type-list-equiv types types-equiv)
           (equal (pprint-type-list types)
                  (pprint-type-list types-equiv)))
  :rule-classes :congruence)

Subtopics

Pprint-type-list