		Search-engine friendly clone of the ACL2 documentation.

Bech32

Bech32-chars-to-octets

Signature
(bech32-chars-to-octets data-chars) → ret-val
Arguments: data-chars — Guard (character-listp data-chars).
Returns: ret-val — Type (true-listp ret-val).

Definitions and Theorems

Function: bech32-chars-to-octets

(defun bech32-chars-to-octets (data-chars)
  (declare (xargs :guard (character-listp data-chars)))
  (let ((__function__ 'bech32-chars-to-octets))
    (declare (ignorable __function__))
    (if (endp data-chars)
        nil
      (cons (position (first data-chars)
                      *bech32-char-vals*)
            (bech32-chars-to-octets (rest data-chars))))))

Theorem: true-listp-of-bech32-chars-to-octets

(defthm true-listp-of-bech32-chars-to-octets
  (b* ((ret-val (bech32-chars-to-octets data-chars)))
    (true-listp ret-val))
  :rule-classes :rewrite)