diff options
Diffstat (limited to 'lists/remove-nth.lisp')
| -rw-r--r-- | lists/remove-nth.lisp | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/lists/remove-nth.lisp b/lists/remove-nth.lisp new file mode 100644 index 0000000..8c62e9d --- /dev/null +++ b/lists/remove-nth.lisp @@ -0,0 +1,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)))) |