		Search-engine friendly clone of the ACL2 documentation.

Addresses

Address-valid-p

Signature
(address-valid-p address) → y/n
Arguments: address — Guard (addressp address).
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: address-valid-p

(defun address-valid-p (address)
  (declare (xargs :guard (addressp address)))
  (let ((__function__ 'address-valid-p))
    (declare (ignorable __function__))
    (let ((addr-string (address->name address)))
      (and (address-string-p addr-string)
           (bitcoin::valid-bech32-or-bech32m addr-string)))))

Theorem: booleanp-of-address-valid-p

(defthm booleanp-of-address-valid-p
  (b* ((y/n (address-valid-p address)))
    (booleanp y/n))
  :rule-classes :rewrite)