collect up all second components of pairs in a list
Major Section:  ACL2-BUILT-INS

(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.

To see the ACL2 definition of this function, see pf.