		Search-engine friendly clone of the ACL2 documentation.

Addresses

Address-string-p

Check if a string forms a Leo address.

Signature
(address-string-p string) → yes/no
Arguments: string — Guard (stringp string).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: address-string-p

(defun address-string-p (string)
  (declare (xargs :guard (stringp string)))
  (let ((__function__ 'address-string-p))
    (declare (ignorable __function__))
    (address-chars-p (acl2::explode string))))

Theorem: booleanp-of-address-string-p

(defthm booleanp-of-address-string-p
  (b* ((yes/no (address-string-p string)))
    (booleanp yes/no))
  :rule-classes :rewrite)