		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Spaces1

Signature
(spaces1 n col hard-right-margin acc) → new-acc
Arguments: n — Guard (natp n).; col — Guard (natp col).; hard-right-margin — Guard (posp hard-right-margin).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: spaces1

(defun spaces1 (n col hard-right-margin acc)
  (declare (xargs :guard (and (natp n)
                              (natp col)
                              (posp hard-right-margin))))
  (let ((acl2::__function__ 'spaces1))
    (declare (ignorable acl2::__function__))
    (b* ((n (nfix n))
         (col (nfix col))
         (hard-right-margin (acl2::pos-fix hard-right-margin)))
      (cond ((zp n) acc)
            ((> col hard-right-margin)
             (spaces1 n 0
                      hard-right-margin (cons #\Newline acc)))
            (t (spaces1 (- n 1)
                        (+ 1 col)
                        hard-right-margin
                        (cons #\Space acc)))))))

Theorem: character-listp-of-spaces1

(defthm character-listp-of-spaces1
  (implies (character-listp acc)
           (b* ((new-acc (spaces1 n col hard-right-margin acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)