fix(frontends/lean): '@' explicit mark

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

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)) {

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