TAKE

initial segment of a list
Major Section:  ACL2-BUILT-INS

For any natural number n not exceeding the length of l, (take n l) collects the first n elements of the list l.

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

(equal (length (take n l)) (nfix n))
If n is an integer greater than the length of l, then take pads the list with the appropriate number of nil elements. Thus, the following is also a theorem.
(implies (and (integerp n)
              (true-listp l)
              (<= (length l) n))
         (equal (take n l)
                (append l (make-list (- n (length l))))))
For related functions, see nthcdr and see butlast.

The guard for (take n l) is that n is a nonnegative integer and l is a true list.

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