From 3dc8f72c32f1c8442613f14eef955b635e16726e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Nov 2015 12:55:50 -0800 Subject: [PATCH] feat(frontends/lean/builtin_cmds): display congr lemma arg mask --- src/frontends/lean/builtin_cmds.cpp | 14 +++++++++++++- src/library/congr_lemma_manager.cpp | 6 ------ 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index ed5f63fa0..b7c924a47 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -1291,7 +1291,19 @@ static environment congr_lemma_cmd(parser & p) { auto r = cm.mk_congr_simp(e); if (!r) throw parser_error("failed to generated congruence lemma", pos); - p.regular_stream() << r->get_proof() << "\n:\n" << r->get_type() << "\n";; + auto out = p.regular_stream(); + out << "["; + bool first = true; + for (auto k : r->get_arg_kinds()) { + if (!first) out << ", "; else first = false; + switch (k) { + case congr_lemma_manager::congr_arg_kind::Fixed: out << "fixed"; break; + case congr_lemma_manager::congr_arg_kind::Eq: out << "eq"; break; + case congr_lemma_manager::congr_arg_kind::Cast: out << "cast"; break; + } + } + out << "]\n"; + out << r->get_proof() << "\n:\n" << r->get_type() << "\n";; type_checker tc(env); expr type = tc.check(r->get_proof(), ls).first; if (!tc.is_def_eq(type, r->get_type()).first) diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp index e63726b73..389967ee7 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma_manager.cpp @@ -95,10 +95,6 @@ class congr_lemma_manager::imp { } optional mk_congr_simp(expr const & fn, buffer const & pinfos, buffer const & kinds) { - for (unsigned i = 0; i < kinds.size(); i++) - std::cout << (unsigned)kinds[i] << " "; - std::cout << "\n"; - expr fn_type = whnf(infer(fn)); name e_name("e"); buffer lhss; @@ -142,8 +138,6 @@ class congr_lemma_manager::imp { eqs.push_back(none_expr()); break; }} - // std::cout << lhss.back() << "\n"; - // std::cout << rhss.back() << "\n\n"; fn_type = whnf(instantiate(binding_body(fn_type), lhs)); } expr lhs = mk_app(fn, lhss);