1 files changed, 28 insertions, 0 deletions
diff --git a/combinations.lisp b/combinations.lisp
new file mode 100644
index 0000000..1867923
--- /dev/null
+++ b/combinations.lisp
@@ -0,0 +1,28 @@
+(defun cons-all (e x)
+  (declare (xargs :guard (true-listp x)))
+  (if (endp x)
+      nil
+      (cons (cons e (car x))
+            (cons-all e (cdr x)))))
+
+(defun combinations (x n)
+  (declare (xargs :guard (and (true-listp x)
+                              (natp n))))
+  (cond
+    ((zp n) (list nil))
+    ((endp x) nil)
+    (t
+     (append (cons-all (car x)
+                       (combinations (cdr x) (- n 1)))
+             (combinations (cdr x) n)))))
+
+(defun comb (n k)
+  (cond
+    ((zp k) 1)
+    ((zp n) 0)
+    (t (+ (comb (- n 1) k)
+          (comb (- n 1) (- k 1))))))
+
+(defthm len-combinations
+  (equal (len (combinations x n))
+         (comb (len x) n)))