		Search-engine friendly clone of the ACL2 documentation.

Nthcdr

Final segment of a list

(Nthcdr n l) removes the first n elements from the list l.

The following is a theorem.

(implies (and (integerp n)
              (<= 0 n)
              (true-listp l))
         (equal (length (nthcdr n l))
                (if (<= n (length l))
                    (- (length l) n)
                  0)))

For related functions, see take and see butlast.

The guard of (nthcdr n l) requires that n is a nonnegative integer and l is a true list.

Nthcdr is a Common Lisp function. See any Common Lisp documentation for more information.

Function: nthcdr

(defun nthcdr (n l)
  (declare (xargs :guard (and (integerp n)
                              (<= 0 n)
                              (true-listp l))))
  (if (zp n) l (nthcdr (+ n -1) (cdr l))))

Subtopics

Std/lists/nthcdr: Lemmas about nthcdr available in the std/lists library.
Nthcdr-theorems: Some theorems about the built-in function nthcdr.
Rest-n: rest-n is identical to nthcdr, but its guard does not require (true-listp x).