The last cons (not element) of a list
(Last l) is the last cons of a list. Here are examples.
ACL2 !>(last '(a b . c)) (B . C) ACL2 !>(last '(a b c)) (C)
(Last l) has a guard of (listp l); thus, l need not be a true-listp.
Last is a Common Lisp function. See any Common Lisp documentation for more information. Unlike Common Lisp, we do not allow an optional second argument for last.
Function: last
(defun last (l) (declare (xargs :guard (listp l))) (if (atom (cdr l)) l (last (cdr l))))
