fix(frontends/lean/builtin_cmds): allow 'check' command to unfold the current module opaque definitions

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

src/frontends/lean/builtin_cmds.cpp

@@ -81,7 +81,8 @@ environment check_cmd(parser & p) {
     e = p.lambda_abstract(section_ps, e);
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     e = p.elaborate(e, false);
-    expr type = type_checker(p.env()).check(e, ls);
+    type_checker tc(p.env(), p.mk_ngen(),  mk_default_converter(p.env(), true));
+    expr type = tc.check(e, ls);
     p.regular_stream() << e << " : " << type << endl;
     return p.env();
 }

src/frontends/lean/parser.h

@@ -147,6 +147,7 @@ public:
     template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
 
     name mk_fresh_name() { return m_ngen.next(); }
+    name_generator mk_ngen() { return m_ngen.mk_child(); }
 
     /** \brief Return the current position information */
     pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }