		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-line

Pretty-print a (non-blank) line of code.

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

The content to print is preceded by indentation according to the current level.

Definitions and Theorems

Function: pprint-line

(defun pprint-line (content level)
  (declare (xargs :guard (and (msgp content) (natp level))))
  (let ((__function__ 'pprint-line))
    (declare (ignorable __function__))
    (msg "~s0~@1~%" (pprint-indent level)
         content)))

Theorem: msgp-of-pprint-line

(defthm msgp-of-pprint-line
  (b* ((line (pprint-line content level)))
    (msgp line))
  :rule-classes :rewrite)

Theorem: pprint-line-of-nfix-level

(defthm pprint-line-of-nfix-level
  (equal (pprint-line content (nfix level))
         (pprint-line content level)))

Theorem: pprint-line-nat-equiv-congruence-on-level

(defthm pprint-line-nat-equiv-congruence-on-level
  (implies (acl2::nat-equiv level level-equiv)
           (equal (pprint-line content level)
                  (pprint-line content level-equiv)))
  :rule-classes :congruence)