Major Section: ACL2-BUILT-INS
For any natural number
n not exceeding the length of
(take n l) collects the first
n elements of the list
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
nis an integer greater than the length of
takepads the list with the appropriate number of
nilelements. 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
l is a true list.
To see the ACL2 definition of this function, see pf.