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

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

diff --git a/tests/lean/run/eq1.lean b/tests/lean/run/eq1.lean
new file mode 100644
index 000000000..5ba3494ce
--- /dev/null
+++ b/tests/lean/run/eq1.lean
@@ -0,0 +1,16 @@
+inductive day :=
+monday, tuesday, wednesday, thursday, friday, saturday, sunday
+
+open day
+
+definition next_weekday : day → day,
+next_weekday monday    := tuesday,
+next_weekday tuesday   := wednesday,
+next_weekday wednesday := thursday,
+next_weekday thursday  := friday,
+next_weekday friday    := monday,
+next_weekday saturday  := monday,
+next_weekday sunday    := monday
+
+example : next_weekday (next_weekday monday) = wednesday :=
+rfl