summaryrefslogtreecommitdiff
path: root/lists/remove-nth.lisp
blob: 8c62e9d9da0cab31184ab75c56d91f1c9cd25b1e (about) (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(in-package "ACL2")

(defun remove-nth (i x)
  (declare (xargs :guard (and (natp i)
                              (true-listp x))))
  (cond ((endp x) nil)
        ((zp i) (cdr x))
        (t
         (cons (car x)
               (remove-nth (1- i) (cdr x))))))

(defthm len-remove-nth
  (implies (and (consp x)
                (< i (len x)))
           (equal (len (remove-nth i x))
                  (- (len x) 1))))

(defthm true-listp-remove-nth
   (implies (true-listp x)
            (true-listp (remove-nth i x))))