		Search-engine friendly clone of the ACL2 documentation.

First-n

(first-n n x) is logically identical to (take n x), but its guard does not require (true-listp x).

Reasoning Note. We leave first-n enabled, so it will just get rewritten into take. You should typically never write a theorem about first-n: write theorems about take instead.

Definitions and Theorems

Function: first-n

(defun first-n (n x)
  (declare (xargs :guard (natp n)))
  (mbe :logic (take n x)
       :exec (cond ((zp n) nil)
                   ((atom x) (make-list n))
                   (t (cons (car x)
                            (first-n (- n 1) (cdr x)))))))