		Search-engine friendly clone of the ACL2 documentation.

Base58

Base58-char=>val

Turn a Base58 character into the corresponding value.

Signature
(base58-char=>val char) → val
Arguments: char — Guard (base58-characterp char).
Returns: val — Type (base58-valuep val).

This is the inverse of base58-val=>char.

Definitions and Theorems

Function: base58-char=>val

(defun base58-char=>val (char)
  (declare (xargs :guard (base58-characterp char)))
  (let ((__function__ 'base58-char=>val))
    (declare (ignorable __function__))
    (index-of (base58-character-fix char)
              *base58-characters*)))

Theorem: base58-valuep-of-base58-char=>val

(defthm base58-valuep-of-base58-char=>val
  (b* ((val (base58-char=>val char)))
    (base58-valuep val))
  :rule-classes :rewrite)

Theorem: base58-char=>val-of-base58-character-fix-char

(defthm base58-char=>val-of-base58-character-fix-char
  (equal (base58-char=>val (base58-character-fix char))
         (base58-char=>val char)))

Theorem: base58-char=>val-base58-character-equiv-congruence-on-char

(defthm base58-char=>val-base58-character-equiv-congruence-on-char
  (implies (base58-character-equiv char char-equiv)
           (equal (base58-char=>val char)
                  (base58-char=>val char-equiv)))
  :rule-classes :congruence)

Subtopics

Base58-val<=>char-inverses-theorems: base58-val=>char and base58-char=>val are mutual inverses.