		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

S-take

Signature
(s-take n x) → *
Arguments: n — Guard (natp n).; x — Guard (true-listp x).

Definitions and Theorems

Function: s-take

(defun s-take (n x)
  (declare (xargs :guard (and (natp n) (true-listp x))))
  (let ((__function__ 's-take))
    (declare (ignorable __function__))
    (b* (((when (zp n)) (bfr-sterm nil))
         ((mv first rest end) (first/rest/end x))
         ((when (and end (eq first nil)))
          '(nil)))
      (bfr-ucons first (s-take (1- n) rest)))))

Theorem: deps-of-s-take

(defthm deps-of-s-take
  (implies (not (pbfr-list-depends-on k p x))
           (not (pbfr-list-depends-on k p (s-take n x)))))

Theorem: s-take-correct

(defthm s-take-correct
  (equal (bfr-list->u (s-take n x) env)
         (loghead n (bfr-list->s x env))))