		Search-engine friendly clone of the ACL2 documentation.

Base64

Base64-revappend-encode

Efficient (revappend-chars (base64-encode x) acc).

Signature
(base64-revappend-encode x acc) → *
Arguments: x — String to be encoded.
Guard (stringp x).; acc — Accumulator for encoded characters (in reverse order).

We leave this enabled; it would be odd to reason about it.

Definitions and Theorems

Function: base64-revappend-encode

(defun base64-revappend-encode (x acc)
  (declare (xargs :guard (stringp x)))
  (declare (type string x))
  (let ((acl2::__function__ 'base64-revappend-encode))
    (declare (ignorable acl2::__function__))
    (mbe :logic (revappend-chars (base64-encode x) acc)
         :exec (b64-encode-str-impl x 0 (length x)
                                    acc))))