		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Append-n

Signature
(append-n count list) → *
Arguments: count — Guard (natp count).

Definitions and Theorems

Function: append-n

(defun append-n (count list)
  (declare (xargs :guard (natp count)))
  (let ((__function__ 'append-n))
    (declare (ignorable __function__))
    (if (zp count)
        nil
      (append-without-guard list (append-n (1- count) list)))))

Theorem: append-n-of-nfix-count

(defthm append-n-of-nfix-count
  (equal (append-n (nfix count) list)
         (append-n count list)))

Theorem: append-n-nat-equiv-congruence-on-count

(defthm append-n-nat-equiv-congruence-on-count
  (implies (acl2::nat-equiv count count-equiv)
           (equal (append-n count list)
                  (append-n count-equiv list)))
  :rule-classes :congruence)