		Search-engine friendly clone of the ACL2 documentation.

Bech32

Hrp-valid-char-code-p

Signature
(hrp-valid-char-code-p x) → y/n
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: hrp-valid-char-code-p

(defun hrp-valid-char-code-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'hrp-valid-char-code-p))
    (declare (ignorable __function__))
    (and (integerp x)
         (<= 33 x)
         (<= x 126))))

Theorem: booleanp-of-hrp-valid-char-code-p

(defthm booleanp-of-hrp-valid-char-code-p
  (b* ((y/n (hrp-valid-char-code-p x)))
    (booleanp y/n))
  :rule-classes :rewrite)