BUTLAST

Major Section:  PROGRAMMING

(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)))

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.