		Search-engine friendly clone of the ACL2 documentation.

Addresses

Find-addresses

Signature
(find-addresses ast-node) → addresses
Returns: addresses — Type (address-listp addresses).

Definitions and Theorems

Function: find-addresses

(defun find-addresses (ast-node)
  (declare (xargs :guard t))
  (let ((__function__ 'find-addresses))
    (declare (ignorable __function__))
    (b* (((unless (consp ast-node)) nil)
         ((when (reserrp ast-node)) nil)
         ((when (addressp ast-node))
          (list ast-node))
         (first-item (car ast-node))
         (first-item-addresses (find-addresses first-item))
         (rest-items (cdr ast-node))
         (rest-item-addresses (find-addresses rest-items)))
      (append first-item-addresses
              rest-item-addresses))))

Theorem: address-listp-of-find-addresses

(defthm address-listp-of-find-addresses
  (b* ((addresses (find-addresses ast-node)))
    (address-listp addresses))
  :rule-classes :rewrite)