		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-initer

Pretty-print an initializer.

Signature
(pprint-initer initer options) → part
Arguments: initer — Guard (initerp initer).; options — Guard (pprint-options-p options).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-initer

(defun pprint-initer (initer options)
 (declare (xargs :guard (and (initerp initer)
                             (pprint-options-p options))))
 (let ((__function__ 'pprint-initer))
  (declare (ignorable __function__))
  (initer-case
   initer
   :single (pprint-expr initer.get (expr-grade-top)
                        options)
   :list
   (msg
     "{~@0}"
     (pprint-comma-sep (pprint-expr-list initer.get (expr-grade-top)
                                         options))))))

Theorem: msgp-of-pprint-initer

(defthm msgp-of-pprint-initer
  (b* ((part (pprint-initer initer options)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-initer-of-initer-fix-initer

(defthm pprint-initer-of-initer-fix-initer
  (equal (pprint-initer (initer-fix initer)
                        options)
         (pprint-initer initer options)))

Theorem: pprint-initer-initer-equiv-congruence-on-initer

(defthm pprint-initer-initer-equiv-congruence-on-initer
  (implies (initer-equiv initer initer-equiv)
           (equal (pprint-initer initer options)
                  (pprint-initer initer-equiv options)))
  :rule-classes :congruence)

Theorem: pprint-initer-of-pprint-options-fix-options

(defthm pprint-initer-of-pprint-options-fix-options
  (equal (pprint-initer initer (pprint-options-fix options))
         (pprint-initer initer options)))

Theorem: pprint-initer-pprint-options-equiv-congruence-on-options

(defthm pprint-initer-pprint-options-equiv-congruence-on-options
  (implies (pprint-options-equiv options options-equiv)
           (equal (pprint-initer initer options)
                  (pprint-initer initer options-equiv)))
  :rule-classes :congruence)