		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-indent

Print an indentation.

Signature
(print-indent pstate) → new-pstate
Arguments: pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

This should be called at the beginning of a line, i.e. at the very beginning of printing (which will be a no-op, since the indentation level is initially 0), or after printing a new-line character.

We multiply the indentation level by the number of spaces for each level, and we print those many spaces (the code of the space character is 32). This is zero spaces, at indent level 0.

Definitions and Theorems

Function: print-indent

(defun print-indent (pstate)
  (declare (xargs :guard (pristatep pstate)))
  (let ((__function__ 'print-indent))
    (declare (ignorable __function__))
    (b* (((pristate pstate) pstate)
         (spaces-to-print (* pstate.indent-level
                             (priopt->indent-size pstate.options))))
      (print-chars (repeat spaces-to-print 32)
                   pstate))))

Theorem: pristatep-of-print-indent

(defthm pristatep-of-print-indent
  (b* ((new-pstate (print-indent pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-indent-of-pristate-fix-pstate

(defthm print-indent-of-pristate-fix-pstate
  (equal (print-indent (pristate-fix pstate))
         (print-indent pstate)))

Theorem: print-indent-pristate-equiv-congruence-on-pstate

(defthm print-indent-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-indent pstate)
                  (print-indent pstate-equiv)))
  :rule-classes :congruence)