		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-one-line

Pretty-print a (non-blank) line of code, as a singleton list of lines.

Signature
(pprint-one-line content level) → lines
Arguments: content — Guard (msgp content).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-one-line

(defun pprint-one-line (content level)
  (declare (xargs :guard (and (msgp content) (natp level))))
  (let ((__function__ 'pprint-one-line))
    (declare (ignorable __function__))
    (list (pprint-line content level))))

Theorem: msg-listp-of-pprint-one-line

(defthm msg-listp-of-pprint-one-line
  (b* ((lines (pprint-one-line content level)))
    (msg-listp lines))
  :rule-classes :rewrite)