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
cdrs). This function is implemented in a tail-recursive
way, despite its logical definition.
To see the ACL2 definition of this function, see pf.