feat(frontends/lean): variables/parameters and check commands have access to all section variables/parameters, closes #231

src/frontends/lean/builtin_cmds.cpp

@@ -130,7 +130,7 @@ environment end_scoped_cmd(parser & p) {
 /** \brief Auxiliary function for check/eval */
 static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
     expr e   = p.parse_expr();
-    list<expr> ctx = locals_to_context(e, p);
+    list<expr> ctx = p.locals_to_context();
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     level_param_names new_ls;
     std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);

src/frontends/lean/decl_cmds.cpp

@@ -167,7 +167,7 @@ environment variable_cmd_core(parser & p, variable_kind k) {
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
     }
     level_param_names new_ls;
-    list<expr> ctx = locals_to_context(type, p);
+    list<expr> ctx = p.locals_to_context();
     std::tie(type, new_ls) = p.elaborate_type(type, ctx);
     update_section_local_levels(p, new_ls, k == variable_kind::Variable);
     return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos);

src/frontends/lean/parser.cpp

@@ -463,6 +463,10 @@ void parser::get_include_variables(buffer<expr> & vars) const {
         });
 }
 
+list<expr> parser::locals_to_context() const {
+    return filter(m_local_decls.get_values(), [](expr const & e) { return is_local(e); });
+}
+
 static unsigned g_level_add_prec = 10;
 static unsigned g_level_cup_prec = 5;
 

tests/lean/const.lean

@@ -0,0 +1,17 @@
+import logic
+
+
+definition foo {A : Type} {H : inhabited A} : A :=
+inhabited.rec (λa, a) H
+
+constant bla {A : Type} {H : inhabited A} : Type.{1}
+
+set_option pp.implicit true
+
+section
+  variable A : Type
+  variable S : inhabited A
+  variable B : bla
+  check B
+  check @foo A _
+end

tests/lean/const.lean.expected.out

@@ -0,0 +1,2 @@
+B : @bla A S
+@foo A S : A