From fd332e411d2ae75949f0bf5515edd73f37288a9e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Jan 2015 12:25:14 -0800
Subject: [PATCH] test(tests/lean/run): add more overlapping patterns examples

---
 tests/lean/run/eq12.lean | 22 ++++++++++++++++++++++
 tests/lean/run/eq13.lean | 16 ++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 tests/lean/run/eq12.lean
 create mode 100644 tests/lean/run/eq13.lean

diff --git a/tests/lean/run/eq12.lean b/tests/lean/run/eq12.lean
new file mode 100644
index 000000000..6fa6fb099
--- /dev/null
+++ b/tests/lean/run/eq12.lean
@@ -0,0 +1,22 @@
+open nat bool inhabited
+
+definition diag : bool → bool → bool → nat,
+diag _  tt ff := 1,
+diag ff _  tt := 2,
+diag tt ff _  := 3,
+diag _  _  _  := default nat
+
+theorem diag1 (a : bool) : diag a tt ff = 1 :=
+bool.cases_on a rfl rfl
+
+theorem diag2 (a : bool) : diag ff a tt = 2 :=
+bool.cases_on a rfl rfl
+
+theorem diag3 (a : bool) : diag tt ff a = 3 :=
+bool.cases_on a rfl rfl
+
+theorem diag4_1 : diag ff ff ff = default nat :=
+rfl
+
+theorem diag4_2 : diag tt tt tt = default nat :=
+rfl
diff --git a/tests/lean/run/eq13.lean b/tests/lean/run/eq13.lean
new file mode 100644
index 000000000..b21753200
--- /dev/null
+++ b/tests/lean/run/eq13.lean
@@ -0,0 +1,16 @@
+open nat inhabited
+
+definition f : nat → nat → nat,
+f _ 0 := 0,
+f 0 _ := 1,
+f _ _ := 2
+
+theorem f_zero_right : ∀ a, f a 0 = 0,
+f_zero_right 0        := rfl,
+f_zero_right (succ _) := rfl
+
+theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
+rfl
+
+theorem f_succ_succ (a b : nat) : f (a+1) (b+1) = 2 :=
+rfl