The last cdr of a list
(Last-cdr x) is x if x is an atom, and otherwise is the last cdr of a list. Here are examples.
ACL2 !>(last-cdr '(a b . c)) C ACL2 !>(last-cdr '(a b c)) NIL
(Last-cdr x) has a guard of t.
Function: last-cdr
(defun last-cdr (x) (declare (xargs :guard t)) (if (atom x) x (cdr (last x))))