max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/simplify): trace prove failures

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-17 11:53:44 -08:00
parent 7d5b866503
commit ac1af2dfda
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/tactic/simplify.cpp
View file

@ -120,6 +120,9 @@ bool simplify_core_fn::instantiate_emetas(tmp_type_context & tmp_ctx, unsigned n
if (auto pf = prove(mvar_type)) {
lean_verify(tmp_ctx.is_def_eq(mvar, *pf));
return;
} else {
lean_simp_trace(tmp_ctx, name({"simplify", "failure"}),
tout() << "failed to prove: " << mvar << " : " << mvar_type << "\n";);
}
}