		Search-engine friendly clone of the ACL2 documentation.

Output-pretty-printer

Pprint-output-item

Pretty-print an output item.

Signature
(pprint-output-item outitem level) → line
Arguments: outitem — Guard (output-itemp outitem).; level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-output-item

(defun pprint-output-item (outitem level)
  (declare (xargs :guard (and (output-itemp outitem)
                              (natp level))))
  (let ((__function__ 'pprint-output-item))
    (declare (ignorable __function__))
    (b* (((output-item outitem) outitem))
      (pprint-line (msg "~@0;"
                        (pprint-output-expression outitem.get))
                   level))))

Theorem: msgp-of-pprint-output-item

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

Theorem: pprint-output-item-of-output-item-fix-outitem

(defthm pprint-output-item-of-output-item-fix-outitem
  (equal (pprint-output-item (output-item-fix outitem)
                             level)
         (pprint-output-item outitem level)))

Theorem: pprint-output-item-output-item-equiv-congruence-on-outitem

(defthm pprint-output-item-output-item-equiv-congruence-on-outitem
  (implies (output-item-equiv outitem outitem-equiv)
           (equal (pprint-output-item outitem level)
                  (pprint-output-item outitem-equiv level)))
  :rule-classes :congruence)

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

(defthm pprint-output-item-of-nfix-level
  (equal (pprint-output-item outitem (nfix level))
         (pprint-output-item outitem level)))

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

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