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

fix(library/congr_lemma_manager): use abstract_local

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-07 12:21:40 -08:00
parent 8a7321714a
commit df94864809
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/congr_lemma_manager.cpp
View file

@ -70,18 +70,18 @@ class congr_lemma_manager::imp {
use_drec = true;
motive = Fun(rhs, Fun(*major, type));
// We compute new_type by replacing rhs with lhs and *major with eq.refl(lhs) in type.
new_type = instantiate(abstract(type, rhs), lhs);
new_type = instantiate(abstract_local(type, rhs), lhs);
auto refl = m_builder.mk_eq_refl(lhs);
if (!refl)
return none_expr();
new_type = instantiate(abstract(new_type, *major), *refl);
new_type = instantiate(abstract_local(new_type, *major), *refl);
} else {
// type does not depend on the *major.
// So, the motive is just (fun rhs, type), and
// new_type just replaces rhs with lhs.
use_drec = false;
motive = Fun(rhs, type);
new_type = instantiate(abstract(type, rhs), lhs);
new_type = instantiate(abstract_local(type, rhs), lhs);
}
auto minor = cast(e, new_type, tail(deps), eqs);
if (!minor)