fix(frontends/lean/elaborator): ignore auto/default params when @ i…

…s used see leanprover#1485 @Kha We need this commit to be able to execute commands such as: ```lean #check @monad.mk ```
leodemoura · Mar 24, 2017 · e97c934 · e97c934
1 parent cf638f6
commit e97c934
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
@@ -1540,8 +1540,11 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
     type = instantiate_mvars(type_before_whnf);
 
     buffer<expr> eta_args;
-    if (optional<expr> new_type = process_optional_and_auto_params(type, ref, eta_args, new_args))
-        type = *new_type;
+    if (amask == arg_mask::Default) {
+        /* We ignore optional/auto params when `@` is used */
+        if (optional<expr> new_type = process_optional_and_auto_params(type, ref, eta_args, new_args))
+            type = *new_type;
+    }
 
     expr r = Fun(eta_args, mk_app(fn, new_args.size(), new_args.data()));
     if (expected_type) {

diff --git a/tests/lean/run/check_monad_mk.lean b/tests/lean/run/check_monad_mk.lean
@@ -0,0 +1,3 @@
+#check @monad.mk
+#check @functor.mk
+#check @applicative.mk