From 3fd452d1dbe8f51cc45b81fd32e5afaae2b83a80 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 Jul 2016 17:38:51 -0700
Subject: [PATCH] test(tests/lean): add new test for overloaded application

---
 tests/lean/elab4.lean              | 23 +++++++++++++++++++++
 tests/lean/elab4.lean.expected.out | 33 ++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+)
 create mode 100644 tests/lean/elab4.lean
 create mode 100644 tests/lean/elab4.lean.expected.out

diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean
new file mode 100644
index 0000000000..bce01b76df
--- /dev/null
+++ b/tests/lean/elab4.lean
@@ -0,0 +1,23 @@
+definition foo.f {A : Type} {B : Type} (a : A) (b : B) : A := a
+
+definition boo.f (a : nat) (b : nat) (c : nat) := a + b + c
+
+definition bla.f (a b c d : bool) := a
+
+open boo foo bla
+
+set_option pp.full_names true
+
+#elab f 0 1 2
+
+#elab f 0 1 2 3
+
+#elab f 0 1
+
+#elab f tt 2
+
+#elab f tt ff tt
+
+#elab f tt ff
+
+#elab @foo.f _ _ 0 1
diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
new file mode 100644
index 0000000000..69c014b55b
--- /dev/null
+++ b/tests/lean/elab4.lean.expected.out
@@ -0,0 +1,33 @@
+>> [choice bla.f foo.f boo.f] [prenum] [prenum] [prenum]
+>> boo.f 0 1 2
+>> ℕ
+>> [choice bla.f foo.f boo.f] [prenum] [prenum] [prenum] [prenum]
+elab4.lean:13:6: error: none of the overloads is applicable
+error for bla.f
+failed to synthesize type class instance for
+  has_zero bool
+
+error for foo.f
+invalid function application, too many arguments, function type:
+  Π {A} {B}, A → B → A
+
+error for boo.f
+invalid function application, too many arguments, function type:
+  ℕ → ℕ → ℕ → ℕ
+>> [choice bla.f foo.f boo.f] [prenum] [prenum]
+elab4.lean:15:6: error: ambiguous overload, possible interpretations
+  foo.f 0 1
+  boo.f 0 1
+>> [choice bla.f foo.f boo.f] bool.tt [prenum]
+>> foo.f bool.tt 2
+>> bool
+>> [choice bla.f foo.f boo.f] bool.tt bool.ff bool.tt
+>> bla.f bool.tt bool.ff bool.tt
+>> bool → bool
+>> [choice bla.f foo.f boo.f] bool.tt bool.ff
+elab4.lean:21:6: error: ambiguous overload, possible interpretations
+  bla.f bool.tt bool.ff
+  foo.f bool.tt bool.ff
+>> @foo.f _ _ [prenum] [prenum]
+>> foo.f 0 1
+>> ℕ