		Search-engine friendly clone of the ACL2 documentation.

Evens

The even-indexed members of a list

The call (evens x) returns the restriction of the true-list x to its even-indexed members (with zero-based indexing). Note that if x is a list (k1 a1 k2 a2 ... kn an) that satisfies the predicate keyword-value-listp, then (evens x) lists the keys ki of x. Thus, the following is a theorem.

(thm (iff (keyword-value-listp l)
          (and (true-listp l)
               (evenp (len l))
               (keyword-listp (evens l))))
     :hints (("Goal" :induct (keyword-value-listp l))))

Function: evens

(defun evens (l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
        (t (cons (car l) (evens (cddr l))))))