		Search-engine friendly clone of the ACL2 documentation.

Butlast

All but a final segment of a list

(Butlast l n) is the list obtained by removing the last n elements from the true list l. The following are theorems.

(implies (and (integerp n)
              (<= 0 n)
              (true-listp l))
         (equal (length (butlast l n))
                (if (< n (length l))
                    (- (length l) n)
                  0)))

(equal (len (butlast l n)) (nfix (- (len l) (nfix n)))))

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.

Function: butlast

(defun butlast (lst n)
  (declare (xargs :guard (and (true-listp lst)
                              (integerp n)
                              (<= 0 n))))
  (let ((lng (len lst)) (n (nfix n)))
    (if (<= lng n)
        nil
      (take (- lng n) lst))))

Subtopics

Std/lists/butlast: Lemmas about butlast available in the std/lists library.