Major Section: ACL2-BUILT-INS
(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
To see the ACL2 definition of this function, see pf.