feat(frontends/lean/elaborator): support for strict implicit arguments

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

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

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