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

feat(library/app_builder): avoid redundant heq_of_eq(eq_of_heq(H)) proofs

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-10 19:29:34 -08:00
parent ddff37dd0f
commit 32268b71d2
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/app_builder.cpp
View file

@ -600,6 +600,8 @@ struct app_builder::imp {
}
expr mk_heq_of_eq(expr const & H) {
if (is_constant(get_app_fn(H), get_eq_of_heq_name()))
return app_arg(H);
expr p = m_ctx->relaxed_whnf(m_ctx->infer(H));
expr A, a, b;
if (!is_eq(p, A, a, b)) {