		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Print-flat-objs

We print the elements of x, separated by spaces. If x is a non-nil atom, we print a dot and then x.

Signature
(print-flat-objs x config eviscp acc) → new-acc
Arguments: config — Guard (printconfig-p config).; eviscp — Guard (booleanp eviscp).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

See the discussion in pflat-p: x here is the what field from some pflat object.

Definitions and Theorems

Function: print-flat-objs

(defun print-flat-objs (x config eviscp acc)
  (declare (xargs :guard (and (printconfig-p config)
                              (booleanp eviscp))))
  (let ((acl2::__function__ 'print-flat-objs))
    (declare (ignorable acl2::__function__))
    (cond ((not x) acc)
          ((or (atom x)
               (and eviscp (evisceratedp x)))
           (b* ((acc (cons #\. acc))
                (acc (cons #\Space acc)))
             (print-flat x config eviscp acc)))
          (t (b* ((acc (print-flat (car x) config eviscp acc))
                  ((unless (cdr x)) acc)
                  (acc (cons #\Space acc)))
               (print-flat-objs (cdr x)
                                config eviscp acc))))))

Theorem: character-listp-of-print-flat-objs

(defthm character-listp-of-print-flat-objs
  (implies (character-listp acc)
           (b* ((new-acc (print-flat-objs x config eviscp acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)