		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)