		Search-engine friendly clone of the ACL2 documentation.

Strip-cdrs

Collect up all second components of pairs in a list

(strip-cdrs x) has a guard of (alistp x), and returns the list obtained by walking through the list x and collecting up all second components (cdrs). This function is implemented in a tail-recursive way, despite its logical definition.

Function: strip-cdrs

(defun strip-cdrs (x)
  (declare (xargs :guard (alistp x)))
  (cond ((endp x) nil)
        (t (cons (cdr (car x))
                 (strip-cdrs (cdr x))))))

Subtopics

Alist-vals: (alist-vals x) collects all values bound in an alist.
Std/alists/strip-cdrs: Lemmas about strip-cdrs available in the std/alists library.