michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/unit/unit_propagate): use ppb when tracing

Browse source
This commit is contained in:
Daniel Selsam 2016-01-27 14:39:46 -08:00 committed by Leonardo de Moura
parent 684995640a
commit 6ed6306c3f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/blast/unit/unit_propagate.cpp
View file

@ -294,7 +294,7 @@ static action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr co
}
curr_state().mk_hypothesis(final_type, final_proof);
lean_trace_unit_propagate(tout() << final_type << "\n";);
lean_trace_unit_propagate(tout() << ppb(final_type) << "\n";);
return action_result::new_branch();
}
@ -316,7 +316,7 @@ static action_result unit_dep_lemma(hypothesis_idx hidx, expr type, expr proof)
if (propagated) {
curr_state().del_hypothesis(hidx);
curr_state().mk_hypothesis(type, proof);
lean_trace_unit_propagate(tout() << type << "\n";);
lean_trace_unit_propagate(tout() << ppb(type) << "\n";);
return action_result::new_branch();
}
lean_assert(is_pi(type));
@ -351,7 +351,7 @@ static action_result unit_fact(expr const & type) {
action_result unit_propagate(unsigned hidx) {
hypothesis const & h = curr_state().get_hypothesis_decl(hidx);
expr type = whnf(h.get_type());
lean_trace_debug_unit_propagate(tout() << type << "\n";);
lean_trace_debug_unit_propagate(tout() << ppb(type) << "\n";);
if (is_lemma(type)) return unit_lemma(hidx, type, h.get_self());
else if (is_dep_lemma(type)) return unit_dep_lemma(hidx, type, h.get_self());
else if (is_fact(type)) return unit_fact(type);