Major Section: PROGRAMMING (Butlast l n) is the list obtained by
removing the last elements from the true list l. The following
is a theorem (though it takes some effort, including lemmas, to
get ACL2 to prove (implies (and (integerp n) (<= 0 n) (true-
listp l)) (equal (length (butlast l n)) (if (< n (length l)) (-
(length l) n) 0)))For related functions, see take and see
nthcdr. The guard for (butlast l n) requires that n is a
nonnegative lst is a true list. Butlast is a Common Lisp
function. See any Common Lisp documentation for more
information. Note: In Common Lisp the second argument of butlast
is optional, but in ACL2 it is