Last
The last cons (not element) of a list
(Last l) is the last cons of a list, l. 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))))
Subtopics
- Std/lists/last
- Lemmas about last available in the std/lists library.
- Last-theorems
- Some theorems about the built-in function last.
