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

chore(library/blast/simplifier/simplifier): use '-->' for tracing a rewrite

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-09 08:06:05 -08:00
parent 6b91505c0e
commit fbaa3e13ab
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/simplifier/simplifier.cpp
View file

@ -602,7 +602,7 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
tout() << "(" << sr.get_id() << ") "
<< "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";);
<< "[" << ppb(new_lhs) << " --> " << ppb(new_rhs) << "]\n";);
if (!instantiate_emetas(tmp_tctx, sr.get_num_emeta(), sr.get_emetas(), sr.get_instances())) return result(e);