		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-title

Pretty-print an input title.

Signature
(pprint-input-title intitle level) → line
Arguments: intitle — Guard (input-titlep intitle).; level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-input-title

(defun pprint-input-title (intitle level)
  (declare (xargs :guard (and (input-titlep intitle)
                              (natp level))))
  (let ((__function__ 'pprint-input-title))
    (declare (ignorable __function__))
    (pprint-line (msg "[~@0]" (input-title->sort intitle))
                 level)))

Theorem: msgp-of-pprint-input-title

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

Theorem: pprint-input-title-of-input-title-fix-intitle

(defthm pprint-input-title-of-input-title-fix-intitle
  (equal (pprint-input-title (input-title-fix intitle)
                             level)
         (pprint-input-title intitle level)))

Theorem: pprint-input-title-input-title-equiv-congruence-on-intitle

(defthm pprint-input-title-input-title-equiv-congruence-on-intitle
  (implies (input-title-equiv intitle intitle-equiv)
           (equal (pprint-input-title intitle level)
                  (pprint-input-title intitle-equiv level)))
  :rule-classes :congruence)

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

(defthm pprint-input-title-of-nfix-level
  (equal (pprint-input-title intitle (nfix level))
         (pprint-input-title intitle level)))

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

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