		Search-engine friendly clone of the ACL2 documentation.

Operations-leaders

Nth-address

The address at a given index in a set of addresses.

Signature
(nth-address index addrs) → addr
Arguments: index — Guard (natp index).; addrs — Guard (address-setp addrs).
Returns: addr — Type (addressp addr).

ACL2 osets are ordered sets, according to ACL2's total order on values, and so they can be treated as lists (without repetitions); in fact, that is exactly how they are represented. In particular, it makes sense to retrieve the element of a set that occupies a given position in the sequential order. As in lists, we index the positions starting from 0.

This could be a more general operation on sets. Another option could be simply to use nth, since osets are lists.

Definitions and Theorems

Function: nth-address

(defun nth-address (index addrs)
  (declare (xargs :guard (and (natp index)
                              (address-setp addrs))))
  (declare (xargs :guard (< index (cardinality addrs))))
  (let ((__function__ 'nth-address))
    (declare (ignorable __function__))
    (cond ((emptyp addrs)
           (prog2$ (impossible)
                   (address :irrelevant)))
          ((zp index) (address-fix (head addrs)))
          (t (nth-address (1- index)
                          (tail addrs))))))

Theorem: addressp-of-nth-address

(defthm addressp-of-nth-address
  (b* ((addr (nth-address index addrs)))
    (addressp addr))
  :rule-classes :rewrite)