		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-annotation

Pretty-print an annotation.

Signature
(pprint-annotation ann level) → line
Arguments: ann — Guard (annotationp ann).; level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-annotation

(defun pprint-annotation (ann level)
  (declare (xargs :guard (and (annotationp ann) (natp level))))
  (let ((__function__ 'pprint-annotation))
    (declare (ignorable __function__))
    (b* (((annotation ann) ann))
      (pprint-line (msg "@~@0" (pprint-identifier ann.name))
                   level))))

Theorem: msgp-of-pprint-annotation

(defthm msgp-of-pprint-annotation
  (b* ((line (pprint-annotation ann level)))
    (msgp line))
  :rule-classes :rewrite)