From 92b6c06a21a79af7609657ee3036b5f5ac0f2bba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Jan 2015 22:22:20 -0800
Subject: [PATCH] test(tests/lean/run): add basic pattern matching compilation
 test

---
 tests/lean/run/eq2.lean | 5 +++++
 tests/lean/run/eq3.lean | 8 ++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 tests/lean/run/eq2.lean
 create mode 100644 tests/lean/run/eq3.lean

diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
new file mode 100644
index 000000000..2ecc6a4a4
--- /dev/null
+++ b/tests/lean/run/eq2.lean
@@ -0,0 +1,5 @@
+definition symm {A : Type} : Π {a b : A}, a = b → b = a,
+symm rfl := rfl
+
+definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c,
+trans rfl rfl := rfl
diff --git a/tests/lean/run/eq3.lean b/tests/lean/run/eq3.lean
new file mode 100644
index 000000000..a1e405782
--- /dev/null
+++ b/tests/lean/run/eq3.lean
@@ -0,0 +1,8 @@
+import data.vector
+open nat vector
+
+definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n)),
+swap (a :: b :: vs) := b :: a :: vs
+
+example (n : nat) (a b : num) (v : vector num n) : swap (a :: b :: v) = b :: a :: v :=
+rfl