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.