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

fix(library/unifier): remove incorrect assertion, a local constant may occur in the type of a metavariable that was not instantiated yet

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-20 18:22:43 -07:00
parent d78c26977b
commit e5057ed155
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/unifier.cpp
View file

@ -1482,7 +1482,6 @@ struct unifier_fn {
} catch (exception&) {} } catch (exception&) {}
expr v = Fun(locals, mk_app(f, sargs)); expr v = Fun(locals, mk_app(f, sargs));
// std::cout << " >> app imitation, v: " << v << "\n"; // std::cout << " >> app imitation, v: " << v << "\n";
lean_assert(!has_local(v));
cs = cs + mk_eq_cnstr(m, v, j, relax); cs = cs + mk_eq_cnstr(m, v, j, relax);
alts.push_back(cs.to_list()); alts.push_back(cs.to_list());
} }