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

feat(library/type_context): improve precision

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-07 12:01:12 -07:00
parent cc3150ea79
commit 224d78e98c
1 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/type_context.cpp
View file

@ -2141,7 +2141,23 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
optional<metavar_decl> m2_decl = m_mctx.get_metavar_decl(f2);
if (m1_decl && m2_decl) {
if (m2_decl->get_context().is_subset_of(m1_decl->get_context())) {
return to_lbool(process_assignment(e1, e2));
if (!is_app(e1) || is_app(e2)) {
return to_lbool(process_assignment(e1, e2));
} else if (m1_decl->get_context().is_subset_of(m2_decl->get_context())) {
lean_assert(is_app(e1) && !is_app(e2));
/* It is easier to solve the assignment
?m2 := ?m1 a_1 ... a_n
than
?m1 a_1 ... a_n := ?m2
Reason: the first one is precise. For example,
consider the following constraint:
?m1 ?m =?= ?m2
*/
return to_lbool(process_assignment(e2, e1));
} else {
return to_lbool(process_assignment(e1, e2));
}
} else {
return to_lbool(process_assignment(e2, e1));
}