		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-file

Pretty-print a file.

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

Definitions and Theorems

Function: pprint-file

(defun pprint-file (file)
  (declare (xargs :guard (filep file)))
  (let ((__function__ 'pprint-file))
    (declare (ignorable __function__))
    (append (pprint-importdecl-list (file->imports file))
            (pprint-programdecl (file->program file)))))

Theorem: msg-listp-of-pprint-file

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