		Search-engine friendly clone of the ACL2 documentation.

Output-pretty-printer

Pprint-output-title

Pretty-print an output title.

Signature
(pprint-output-title level) → line
Arguments: level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-output-title

(defun pprint-output-title (level)
  (declare (xargs :guard (natp level)))
  (let ((__function__ 'pprint-output-title))
    (declare (ignorable __function__))
    (pprint-line "[output]" level)))

Theorem: msgp-of-pprint-output-title

(defthm msgp-of-pprint-output-title
  (b* ((line (pprint-output-title level)))
    (msgp line))
  :rule-classes :rewrite)

Theorem: pprint-output-title-of-nfix-level

(defthm pprint-output-title-of-nfix-level
  (equal (pprint-output-title (nfix level))
         (pprint-output-title level)))

Theorem: pprint-output-title-nat-equiv-congruence-on-level

(defthm pprint-output-title-nat-equiv-congruence-on-level
  (implies (acl2::nat-equiv level level-equiv)
           (equal (pprint-output-title level)
                  (pprint-output-title level-equiv)))
  :rule-classes :congruence)