### NTHCDR

final segment of a list
Major Section: ACL2-BUILT-INS

`(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.

To see the ACL2 definition of this function, see pf.