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

feat(library/class): allow transitive instances that have instances arguments

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-30 14:53:33 -07:00
parent 9a9e975bc8
commit 880f212494
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/class.cpp
View file

@ -290,13 +290,13 @@ static pair<name, name> get_source_target(environment const & env, type_checker
if (!tgt) if (!tgt)
throw exception(sstream() << "invalid transitive instance, resulting type of '" << n << "' is not a class"); throw exception(sstream() << "invalid transitive instance, resulting type of '" << n << "' is not a class");
optional<name> src; optional<name> src;
for (expr const & d : domain) { unsigned i = domain.size();
while (i > 0) {
--i;
expr const & d = domain[i];
if (auto it = is_ext_class(tc, mlocal_type(d))) { if (auto it = is_ext_class(tc, mlocal_type(d))) {
if (src) {
throw exception(sstream() << "invalid transitive instance, '" << n
<< "' has more than one instance argument");
}
src = it; src = it;
break;
} }
} }
if (!src) if (!src)