		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing

Revappend-pretty

Pretty-print any ACL2 object, in reverse order, onto a reverse-order character list.

Signature
(revappend-pretty x acc &key (config '*default-printconfig*) (col '0) (eviscp 'nil)) → new-acc
Arguments: x — The ACL2 object to pretty-print.; acc — The reverse-order character list to print to.; config — Optional pretty-printer configuration options.
Guard (printconfig-p config).; col — Optional starting column number.
Guard (natp col).; eviscp — Optional flag for use with eviscerated objects.
Guard (booleanp eviscp).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

This is very similar to pretty, except that it can be used to extend existing character lists. See for instance the discussion in revappend-chars.

Definitions and Theorems

Function: revappend-pretty-fn

(defun revappend-pretty-fn (x acc config col eviscp)
  (declare (xargs :guard (and (printconfig-p config)
                              (natp col)
                              (booleanp eviscp))))
  (let ((acl2::__function__ 'revappend-pretty))
    (declare (ignorable acl2::__function__))
    (ppr x col config eviscp acc)))

Theorem: character-listp-of-revappend-pretty

(defthm character-listp-of-revappend-pretty
  (implies
       (character-listp acc)
       (b* ((new-acc (revappend-pretty-fn x acc config col eviscp)))
         (character-listp new-acc)))
  :rule-classes :rewrite)