From 4416d9b2c56f9a8a82a20ecd9dad8a8ee4592a69 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2015 15:56:41 -0700
Subject: [PATCH] test(tests/lean/run): add basic tests for finset module

---
 tests/lean/run/finset1.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 tests/lean/run/finset1.lean

diff --git a/tests/lean/run/finset1.lean b/tests/lean/run/finset1.lean
new file mode 100644
index 000000000..3d095a78e
--- /dev/null
+++ b/tests/lean/run/finset1.lean
@@ -0,0 +1,17 @@
+import data.finset
+open nat list finset
+
+example : to_finset [1, 3, 1] = to_finset [3, 3, 3, 1] :=
+dec_trivial
+
+example : to_finset [1, 2] ∪ to_finset [1, 3] = to_finset [3, 2, 1] :=
+dec_trivial
+
+example : 1 ∈ to_finset [3, 2, 1] :=
+dec_trivial
+
+example : bigsum (to_finset [3, 2, 2]) (λ x, x*x) = 13 :=
+rfl
+
+example : bigprod (to_finset [1, 2]) (λ x, x+1) = 6 :=
+rfl