		Search-engine friendly clone of the ACL2 documentation.

Base64

Base64-revappend-decode

Efficiently revappend the characters from base64-decode onto an accumulator.

Signature
(base64-revappend-decode x acc) → (mv okp acc)
Arguments: x — String to be decoded.
Guard (stringp x).; acc — Accumulator for decoded characters (in reverse order).
Returns: okp — Was decoding successful?.

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

Definitions and Theorems

Function: base64-revappend-decode

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