### BUTLAST

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

`(Butlast l n)`

is the list obtained by removing the last `n`

elements from the true list `l`

. The following is a theorem
(though it takes some effort, including lemmas, to get ACL2 to prove
it).

(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
integer and `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
required.

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