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

fix(frontends/lean/elaborator): incorrect assertion

Browse source 
It is supposed to be "!first implies is_local(from)"

fixes #807
This commit is contained in:
Leonardo de Moura 2015-08-20 17:55:33 -07:00
parent c32a95bb13
commit 3747ba095a
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1483,7 +1483,7 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
expr r = process_obtain_expr(tail(s_list), tail(from_list), new_goal, false, cs, src); expr r = process_obtain_expr(tail(s_list), tail(from_list), new_goal, false, cs, src);
return Fun(new_from, r); return Fun(new_from, r);
} else { } else {
lean_assert(!first || is_local(from)); lean_assert(first || is_local(from));
expr from_type = whnf(infer_type(from, cs), cs); expr from_type = whnf(infer_type(from, cs), cs);
buffer<expr> I_args; buffer<expr> I_args;
expr I = get_app_args(from_type, I_args); expr I = get_app_args(from_type, I_args);