Major Section: ACL2-BUILT-INS
(Nthcdr n l) removes the first
n elements from the list
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
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.