		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-item

Pretty-print an input item.

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

Definitions and Theorems

Function: pprint-input-item

(defun pprint-input-item (initem level)
  (declare (xargs :guard (and (input-itemp initem)
                              (natp level))))
  (let ((__function__ 'pprint-input-item))
    (declare (ignorable __function__))
    (b* (((input-item initem) initem))
      (pprint-line (msg "~@0: ~@1 = ~@2;"
                        (pprint-identifier initem.name)
                        (pprint-input-type initem.type)
                        (pprint-input-expression initem.value))
                   level))))

Theorem: msgp-of-pprint-input-item

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

Theorem: pprint-input-item-of-input-item-fix-initem

(defthm pprint-input-item-of-input-item-fix-initem
  (equal (pprint-input-item (input-item-fix initem)
                            level)
         (pprint-input-item initem level)))

Theorem: pprint-input-item-input-item-equiv-congruence-on-initem

(defthm pprint-input-item-input-item-equiv-congruence-on-initem
  (implies (input-item-equiv initem initem-equiv)
           (equal (pprint-input-item initem level)
                  (pprint-input-item initem-equiv level)))
  :rule-classes :congruence)

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

(defthm pprint-input-item-of-nfix-level
  (equal (pprint-input-item initem (nfix level))
         (pprint-input-item initem level)))

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

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