From 47ff300d1ac82412e9e2e3fb4e92264806880458 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 28 Jun 2014 07:30:36 -0700
Subject: [PATCH] fix(frontends/lean): '@' explicit mark

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/logic.lean       |  2 +-
 src/frontends/lean/elaborator.cpp | 15 ++++++++++-----
 tests/lean/run/imp.lean           | 28 ++++++++++++++++++++++++++++
 3 files changed, 39 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/imp.lean

diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index d42d888cba..6fb790d0ca 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -59,7 +59,7 @@ inductive eq {A : Type} (a : A) : A → Bool :=
 infix `=` 50 := eq
 
 theorem refl {A : Type} (a : A) : a = a
-:= @(@eq_intro A) a -- TODO: fix '@', we should not need to use two '@'
+:= @eq_intro A a
 
 theorem subst {A : Type} {a b : A} {P : A → Bool} (H1 : a = b) (H2 : P a) : P b
 := eq_rec H2 H1
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index b7da5ac3f3..a5c2287288 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -378,16 +378,19 @@ public:
     }
 
     expr visit_app(expr const & e) {
+        bool expl   = is_explicit(get_app_fn(e));
         expr f      = visit(app_fn(e));
         auto f_t    = ensure_fun(f);
         f           = f_t.first;
         expr f_type = f_t.second;
         lean_assert(is_pi(f_type));
-        while (is_pi(f_type) && binding_info(f_type).is_strict_implicit()) {
-            tag g        = f.get_tag();
-            expr imp_arg = mk_meta(some_expr(binding_domain(f_type)), g);
-            f            = mk_app(f, imp_arg, g);
-            f_type       = whnf(instantiate(binding_body(f_type), imp_arg));
+        if (!expl) {
+            while (is_pi(f_type) && binding_info(f_type).is_strict_implicit()) {
+                tag g        = f.get_tag();
+                expr imp_arg = mk_meta(some_expr(binding_domain(f_type)), g);
+                f            = mk_app(f, imp_arg, g);
+                f_type       = whnf(instantiate(binding_body(f_type), imp_arg));
+            }
         }
         expr d_type = binding_domain(f_type);
         expr a      = visit_expecting_type_of(app_arg(e), d_type);
@@ -547,6 +550,8 @@ public:
         expr r;
         if (is_explicit(e)) {
             r    = visit_core(get_explicit_arg(e));
+        } else if (is_explicit(get_app_fn(e))) {
+            r    = visit_core(e);
         } else {
             r    = visit_core(e);
             if (!is_lambda(r)) {
diff --git a/tests/lean/run/imp.lean b/tests/lean/run/imp.lean
new file mode 100644
index 0000000000..022b1ee441
--- /dev/null
+++ b/tests/lean/run/imp.lean
@@ -0,0 +1,28 @@
+variable N : Type.{1}
+variables a b c : N
+variable f : forall {a b : N}, N → N
+
+check f
+check @f
+check @f a
+check @f a b
+check @f a b c
+
+definition l1 : N → N → N → N := @f
+definition l2 : N → N → N := @f a
+definition l3 : N → N := @f a b
+definition l4 : N := @f a b c
+
+variable g : forall ⦃a b : N⦄, N → N
+
+check g
+check @g
+check @g a
+check @g a b
+check @g a b c
+
+definition l5 : N → N → N → N := @g
+definition l6 : N → N → N := @g a
+definition l7 : N → N := @g a b
+definition l8 : N := @g a b c
+definition l9 : N → N → N → N := g