From 6bf905aea8d211a7a281b67069dfc697b964038e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Sep 2014 09:38:36 -0700 Subject: [PATCH] fix(frontends/lean/pp): do not invoke type checker on expressions containing free variables. This could happened when the pretty printer was used from Lua to print nested subterms --- src/frontends/lean/pp.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 5aa218e3c4..2a95cf068e 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -183,6 +183,10 @@ format pretty_fn::pp_level(level const & l) { bool pretty_fn::is_implicit(expr const & f) { if (m_implict) return false; // showing implicit arguments + if (!closed(f)) { + // the Lean type checker assumes expressions are closed. + return false; + } try { binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first); return bi.is_implicit() || bi.is_strict_implicit(); @@ -320,6 +324,10 @@ auto pretty_fn::pp_local(expr const & e) -> result { } bool pretty_fn::has_implicit_args(expr const & f) { + if (!closed(f)) { + // the Lean type checker assumes expressions are closed. + return false; + } name_generator ngen(*g_tmp_prefix); try { expr type = m_tc.whnf(m_tc.infer(f).first).first;