		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Spaces

Signature
(spaces n col config acc) → new-acc
Arguments: n — Guard (natp n).; col — Guard (natp col).; config — Guard (printconfig-p config).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: spaces

(defun spaces (n col config acc)
  (declare (xargs :guard (and (natp n)
                              (natp col)
                              (printconfig-p config))))
  (let ((acl2::__function__ 'spaces))
    (declare (ignorable acl2::__function__))
    (b* (((printconfig config) config)
         (result-col (+ n col))
         ((when (<= result-col config.hard-right-margin))
          (make-list-ac n #\Space acc)))
      (spaces1 n col config.hard-right-margin acc))))

Theorem: character-listp-of-spaces

(defthm character-listp-of-spaces
  (implies (character-listp acc)
           (b* ((new-acc (spaces n col config acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)