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