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

fix(frontends/lean/elaborator): missing constraint

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-08 19:09:18 -07:00
parent 5087f03889
commit d9afb3ca96
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -781,11 +781,13 @@ public:
f_type = whnf(f_type, cs);
if (!is_pi(f_type) && has_metavar(f_type)) {
constraint_seq saved_cs = cs;
f_type = whnf(f_type, cs);
if (!is_pi(f_type) && is_meta(f_type)) {
expr new_f_type = whnf(f_type, cs);
if (!is_pi(new_f_type) && is_meta(new_f_type)) {
cs = saved_cs;
// let type checker add constraint
f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
} else {
f_type = new_f_type;
}
}
if (!is_pi(f_type)) {