		Search-engine friendly clone of the ACL2 documentation.

Bech32

Hrp-valid-string-length-p

Signature
(hrp-valid-string-length-p s) → y/n
Arguments: s — Guard (stringp s).
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: hrp-valid-string-length-p

(defun hrp-valid-string-length-p (s)
  (declare (xargs :guard (stringp s)))
  (let ((__function__ 'hrp-valid-string-length-p))
    (declare (ignorable __function__))
    (let ((slen (length s)))
      (and (<= 1 slen) (<= slen 83)))))

Theorem: booleanp-of-hrp-valid-string-length-p

(defthm booleanp-of-hrp-valid-string-length-p
  (b* ((y/n (hrp-valid-string-length-p s)))
    (booleanp y/n))
  :rule-classes :rewrite)