		Search-engine friendly clone of the ACL2 documentation.

Take

Initial segment (first n elements) of a list

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:

(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 (though it takes some effort, including lemmas, to get ACL2 to prove it).

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

Function: first-n-ac

(defun first-n-ac (i l ac)
  (declare (type (integer 0 *) i)
           (xargs :guard (and (true-listp l) (true-listp ac))))
  (cond ((zp i) (revappend ac nil))
        (t (first-n-ac (1- i)
                       (cdr l)
                       (cons (car l) ac)))))

Function: take

(defun take (n l)
  (declare (xargs :guard (and (integerp n)
                              (not (< n 0))
                              (true-listp l))))
  (mbe :logic
       (if (zp n)
           nil
         (cons (car l) (take (1- n) (cdr l))))
       :exec (first-n-ac n l nil)))

Subtopics

Std/lists/take: Lemmas about take available in the std/lists library.
First-n: (first-n n x) is logically identical to (take n x), but its guard does not require (true-listp x).
Take-theorems: Some theorems about the built-in function take.