### 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.