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

fix(library/app_builder): do not try to instantiate type class instances that have been explicitly provided

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-20 19:42:21 -04:00
parent 31e0d9d183
commit a50cbf07ab
1 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/app_builder.cpp
View file

@ -260,17 +260,23 @@ class app_builder {
for (optional<expr> const & inst_arg : e.m_inst_args) {
lean_assert(i > 0);
--i;
if (inst_arg) {
expr type = m_ctx.instantiate_mvars(mlocal_type(*inst_arg));
if (auto v = m_ctx.mk_class_instance(type)) {
if (!m_ctx.is_def_eq(*inst_arg, *v))
if (!m_ctx.get_tmp_mvar_assignment(i)) {
if (inst_arg) {
expr type = m_ctx.instantiate_mvars(mlocal_type(*inst_arg));
if (auto v = m_ctx.mk_class_instance(type)) {
if (!m_ctx.is_def_eq(*inst_arg, *v)) {
// failed to assign instance
return false;
}
} else {
// failed to generate instance
return false;
}
} else {
// unassined metavar
return false;
}
}
if (!m_ctx.get_tmp_mvar_assignment(i))
return false;
}
for (unsigned i = 0; i < e.m_num_umeta; i++) {
if (!m_ctx.get_tmp_uvar_assignment(i))