From f8b48ac9558b593280e873802d73eba7d1b08eff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Jul 2016 10:38:59 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): support for strict implicit
 arguments

---
 src/frontends/lean/elaborator.cpp  |  2 ++
 tests/lean/elab6.lean              | 17 +++++++++++++++++
 tests/lean/elab6.lean.expected.out | 20 ++++++++++++++++++++
 3 files changed, 39 insertions(+)
 create mode 100644 tests/lean/elab6.lean
 create mode 100644 tests/lean/elab6.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3b24ca2d8d..7ef99d631e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -539,6 +539,8 @@ expr elaborator::visit_default_app_core(expr const & fn, arg_mask amask, buffer<
         binder_info const & bi = binding_info(type);
         expr const & d = binding_domain(type);
         expr new_arg;
+        if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size())
+            break;
         if ((amask == arg_mask::Default && !is_explicit(bi)) ||
             (amask == arg_mask::Simple && !bi.is_inst_implicit() && !is_first_order(d))) {
             // implicit argument
diff --git a/tests/lean/elab6.lean b/tests/lean/elab6.lean
new file mode 100644
index 0000000000..108bde2489
--- /dev/null
+++ b/tests/lean/elab6.lean
@@ -0,0 +1,17 @@
+constant R : nat → nat → Prop
+constant H : transitive R
+set_option pp.all true
+
+constant F : ∀ {A : Type} ⦃a : A⦄ {b : A} (c : A) ⦃e : A⦄, A → A → A
+
+check H
+check F
+check F tt
+check F tt tt
+check F tt tt tt
+
+#elab H
+#elab F
+#elab F tt
+#elab F tt tt
+#elab F tt tt tt
diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/elab6.lean.expected.out
new file mode 100644
index 0000000000..18ed7467af
--- /dev/null
+++ b/tests/lean/elab6.lean.expected.out
@@ -0,0 +1,20 @@
+H : @transitive.{1} nat R
+@F.{l_1} ?A : Π ⦃a : ?A⦄ {b : ?A}, ?A → (Π ⦃e : ?A⦄, ?A → ?A → ?A)
+@F.{1} bool ?a ?b bool.tt : Π ⦃e : bool⦄, bool → bool → bool
+@F.{1} bool ?a ?b bool.tt ?e bool.tt : bool → bool
+@F.{1} bool ?a ?b bool.tt ?e bool.tt bool.tt : bool
+>> H
+>> H
+>> @transitive.{1} nat R
+>> F
+>> @F.{?M_1} ?M_2
+>> ∀ ⦃a : ?M_2⦄ {b : ?M_2}, ?M_2 → (∀ ⦃e : ?M_2⦄, ?M_2 → ?M_2 → ?M_2)
+>> F bool.tt
+>> @F.{1} bool ?M_1 ?M_2 bool.tt
+>> Π ⦃e : bool⦄, bool → bool → bool
+>> F bool.tt bool.tt
+>> @F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt
+>> bool → bool
+>> F bool.tt bool.tt bool.tt
+>> @F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt
+>> bool