lists: remove-nth, shuffle: Add remove-nth and shuffle.

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))))