		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-file

Pretty-print an input file.

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

Definitions and Theorems

Function: pprint-input-file

(defun pprint-input-file (infile)
  (declare (xargs :guard (input-filep infile)))
  (let ((__function__ 'pprint-input-file))
    (declare (ignorable __function__))
    (pprint-input-section-list (input-file->sections infile))))

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

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