		Search-engine friendly clone of the ACL2 documentation.

Output-pretty-printer

Pprint-output-file

Pretty-print an output file.

Signature
(pprint-output-file outfile) → lines
Arguments: outfile — Guard (output-filep outfile).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-output-file

(defun pprint-output-file (outfile)
  (declare (xargs :guard (output-filep outfile)))
  (let ((__function__ 'pprint-output-file))
    (declare (ignorable __function__))
    (pprint-output-section (output-file->get outfile))))

Theorem: msg-listp-of-pprint-output-file

(defthm msg-listp-of-pprint-output-file
  (b* ((lines (pprint-output-file outfile)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: pprint-output-file-of-output-file-fix-outfile

(defthm pprint-output-file-of-output-file-fix-outfile
  (equal (pprint-output-file (output-file-fix outfile))
         (pprint-output-file outfile)))

Theorem: pprint-output-file-output-file-equiv-congruence-on-outfile

(defthm pprint-output-file-output-file-equiv-congruence-on-outfile
  (implies (output-file-equiv outfile outfile-equiv)
           (equal (pprint-output-file outfile)
                  (pprint-output-file outfile-equiv)))
  :rule-classes :congruence)