		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Cap-length

Signature
(cap-length n x) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: cap-length

(defun cap-length (n x)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'cap-length))
    (declare (ignorable __function__))
    (if (< (lnfix n) (len x))
        (take n (list-fix x))
      x)))

Theorem: cap-length-of-nfix-n

(defthm cap-length-of-nfix-n
  (equal (cap-length (nfix n) x)
         (cap-length n x)))

Theorem: cap-length-nat-equiv-congruence-on-n

(defthm cap-length-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (cap-length n x)
                  (cap-length n-equiv x)))
  :rule-classes :congruence)