From 32a605e793719634276f34a6c185422294600ca1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Jul 2014 17:39:49 -0700 Subject: [PATCH] fix(frontends/lean/builtin_cmds): allow 'check' command to unfold the current module opaque definitions Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 3 ++- src/frontends/lean/parser.h | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 606e75711..140ede3fb 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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(); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 19b991ca0..4cb7af499 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -147,6 +147,7 @@ public: template 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()); }