		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-indent

Pretty-print identation spaces.

Signature
(pprint-indent level) → part
Arguments: level — Guard (natp level).
Returns: part — Type (msgp part).

The non-blank content of each line is indented at a certain level. The level is passed as argument here. We indent by increments of 4 spaces; this could be an option in the future. Thus, we return a string (which is also a message) consisting of a number of spaces equal to 4 times the level.

Definitions and Theorems

Function: pprint-indent

(defun pprint-indent (level)
  (declare (xargs :guard (natp level)))
  (let ((__function__ 'pprint-indent))
    (declare (ignorable __function__))
    (implode (repeat (* 4 (lnfix level)) #\Space))))

Theorem: msgp-of-pprint-indent

(defthm msgp-of-pprint-indent
  (b* ((part (pprint-indent level)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-indent-of-nfix-level

(defthm pprint-indent-of-nfix-level
  (equal (pprint-indent (nfix level))
         (pprint-indent level)))

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

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