		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Atj-indent

Spaces from the left margin for the specified level of indentation.

Signature
(atj-indent level) → spaces
Arguments: level — Guard (natp level).
Returns: spaces — Type (stringp spaces).

We indent by increments of 4 spaces.

Definitions and Theorems

Function: atj-indent

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

Theorem: stringp-of-atj-indent

(defthm stringp-of-atj-indent
  (b* ((spaces (atj-indent level)))
    (stringp spaces))
  :rule-classes :rewrite)