feat(frontends/lean): improve 'check' command when used inside sections

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

src/frontends/lean/builtin_cmds.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/option_declarations.h"
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
@@ -90,7 +91,14 @@ environment check_cmd(parser & p) {
     std::tie(e, new_ls) = p.elaborate_relaxed(e);
     auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
     expr type = tc->check(e, append(ls, new_ls));
-
+    // consume sections_ps introduced with mk_section_params
+    for (unsigned i = 0; i < section_ps.size(); i++) {
+        lean_assert(is_lambda(e));
+        lean_assert(is_pi(type));
+        expr local = mk_local(binding_name(e), binding_domain(e), binding_info(e));
+        e    = instantiate(binding_body(e), local);
+        type = instantiate(binding_body(type), local);
+    }
     formatter fmt = p.ios().get_formatter();
     options opts  = p.ios().get_options();
     unsigned indent = get_pp_indent(opts);

tests/lean/interactive/t3.input.expected.out

@@ -1,3 +1,3 @@
-λ (A : Type), A : Type → Type
-λ (A : Type), A : Type → Type
+A : Type
+A : Type
 done

tests/lean/t4.lean.expected.out

@@ -5,9 +5,9 @@ F : Type → Type
 F : Type → Type
 f : N → N → N
 len : Π (A : Type) (n : N), vec A n → N
-λ (B : Bool), B → B : Bool → Bool
-λ (A : Type), A → A : Type → Type
-λ (C : Type), C : Type → Type
+B → B_1 : Bool
+A → A_1 : Type
+C : Type
 t4.lean:25:6: error: unknown identifier 'A'
 R : Type → Bool
 λ (x y : N), x : N → N → N