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

Fix bug in is_convertible

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-06 16:44:22 -07:00
parent 3ff3eb6444
commit 4c28cb933b
1 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/kernel/type_check.cpp
View file

@ -17,11 +17,21 @@ namespace lean {
bool is_convertible_core(expr const & expected, expr const & given, environment const & env) {
if (expected == given)
return true;
if (is_type(expected) && is_type(given)) {
if (env.is_ge(ty_level(expected), ty_level(given)))
return true;
expr const * e = &expected;
expr const * g = &given;
while (true) {
if (is_type(*e) && is_type(*g)) {
if (env.is_ge(ty_level(*e), ty_level(*g)))
return true;
}
if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
e = &abst_body(*e);
g = &abst_body(*g);
}
else {
return false;
}
}
return false;
}
bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) {