		Search-engine friendly clone of the ACL2 documentation.

Base64-impl

B64-encode-list-impl

Tail-recursive version of base64-encode-list.

Signature
(b64-encode-list-impl x acc) → acc
Arguments: x — Guard (character-listp x).
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: b64-encode-list-impl

(defun b64-encode-list-impl (x acc)
  (declare (xargs :guard (character-listp x)))
  (let ((acl2::__function__ 'b64-encode-list-impl))
    (declare (ignorable acl2::__function__))
    (b* (((when (atom x)) acc)
         ((when (atom (cdddr x)))
          (b* (((mv c1 c2 c3 c4)
                (b64-encode-last-group x)))
            (list* c4 c3 c2 c1 acc)))
         ((mv c1 c2 c3 c4)
          (b64-enc3 (first x)
                    (second x)
                    (third x)))
         (acc (list* c4 c3 c2 c1 acc)))
      (b64-encode-list-impl (cdddr x) acc))))

Theorem: character-listp-of-b64-encode-list-impl

(defthm character-listp-of-b64-encode-list-impl
  (implies (character-listp acc)
           (b* ((acc (b64-encode-list-impl x acc)))
             (character-listp acc)))
  :rule-classes :rewrite)