From eb0b688da8764ffed48d72d73d950517807aaaea Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Mon, 19 Oct 2015 19:14:06 -0400 Subject: [PATCH] style(library/norm_num): remove debug code --- src/library/norm_num.cpp | 1 - src/library/tactic/norm_num_tactic.cpp | 11 +++++------ 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp index 1088b0b2be..ab3da75e26 100644 --- a/src/library/norm_num.cpp +++ b/src/library/norm_num.cpp @@ -344,7 +344,6 @@ pair norm_num_context::mk_norm_mul(expr const & lhs, expr const & rh rv = mk_app({rhs_head, type, typec, mtp.first}); prf = mk_app({mk_const(*g_mul_bit0), type, mk_has_distrib(typec), lhs, args_rhs[2], mtp.first, mtp.second}); } else if (is_bit1(rhs)) { - std::cout << "is_bit1 " << rhs << "\n"; auto mtp = mk_norm_mul(lhs, args_rhs[3]); auto atp = mk_norm_add(mk_app({mk_const(*g_bit0), type, args_rhs[2], mtp.first}), lhs); rv = atp.first; diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp index bffcc0947c..9e8ac164fb 100644 --- a/src/library/tactic/norm_num_tactic.cpp +++ b/src/library/tactic/norm_num_tactic.cpp @@ -33,18 +33,17 @@ tactic norm_num_tactic() { g.get_hyps(hyps); local_context ctx(to_list(hyps)); try { - //bool bs = is_numeral(env, lhs); pair p = mk_norm_num(env, ctx, lhs); expr new_lhs = p.first; expr new_lhs_pr = p.second; pair p2 = mk_norm_num(env, ctx, rhs); expr new_rhs = p2.first; expr new_rhs_pr = p2.second; - //if (new_lhs != new_rhs) { - // std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n"; - // throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs normal form doesn't match rhs"); - // return none_proof_state(); - //} + /*if (new_lhs != new_rhs) { + std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n"; + throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs normal form doesn't match rhs"); + return none_proof_state(); + }*/ type_checker tc(env); expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr)); substitution new_subst = s.get_subst();