		Search-engine friendly clone of the ACL2 documentation.

Base58-character

Base58-characterp

Recognizer for base58-character.

Signature
(base58-characterp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: base58-characterp

(defun base58-characterp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'base58-characterp))
    (declare (ignorable __function__))
    (if (member x *base58-characters*)
        t
      nil)))

Theorem: booleanp-of-base58-characterp

(defthm booleanp-of-base58-characterp
  (b* ((yes/no (base58-characterp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: characterp-when-base58-characterp

(defthm characterp-when-base58-characterp
  (implies (base58-characterp x)
           (characterp x))
  :rule-classes :compound-recognizer)