		Search-engine friendly clone of the ACL2 documentation.

Addresses

Address-chars-p

Check if a list of characters forms a Leo address.

Signature
(address-chars-p chars) → yes/no
Arguments: chars — Guard (character-listp chars).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: address-chars-p

(defun address-chars-p (chars)
  (declare (xargs :guard (character-listp chars)))
  (let ((__function__ 'address-chars-p))
    (declare (ignorable __function__))
    (b* ((chars (str::character-list-fix chars)))
      (and (= (len chars) 63)
           (equal (take 5 chars)
                  (acl2::explode "aleo1"))
           (str::lcletter/digit-charlist-p (nthcdr 5 chars))))))

Theorem: booleanp-of-address-chars-p

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