		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-expression

Pretty-print an input expression.

Signature
(pprint-input-expression inexpr) → part
Arguments: inexpr — Guard (input-expressionp inexpr).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-input-expression

(defun pprint-input-expression (inexpr)
  (declare (xargs :guard (input-expressionp inexpr)))
  (let ((__function__ 'pprint-input-expression))
    (declare (ignorable __function__))
    (pprint-expression (input-expression->get inexpr)
                       (expr-grade-top))))

Theorem: msgp-of-pprint-input-expression

(defthm msgp-of-pprint-input-expression
  (b* ((part (pprint-input-expression inexpr)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-input-expression-of-input-expression-fix-inexpr

(defthm pprint-input-expression-of-input-expression-fix-inexpr
  (equal (pprint-input-expression (input-expression-fix inexpr))
         (pprint-input-expression inexpr)))

Theorem: pprint-input-expression-input-expression-equiv-congruence-on-inexpr

(defthm
 pprint-input-expression-input-expression-equiv-congruence-on-inexpr
 (implies (input-expression-equiv inexpr inexpr-equiv)
          (equal (pprint-input-expression inexpr)
                 (pprint-input-expression inexpr-equiv)))
 :rule-classes :congruence)