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

fix(library/app_builder): bug in eq_drec

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-06 19:06:20 -08:00
parent 34d5882b9a
commit 2d04156959
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/library/app_builder.cpp
View file

@ -440,7 +440,7 @@ struct app_builder::imp {
return none_expr();
expr A = m_ctx->infer(lhs);
auto A_lvl = get_level(A);
expr mtype = m_ctx->whnf(m_ctx->infer(H1));
expr mtype = m_ctx->whnf(m_ctx->infer(motive));
if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype))))
return none_expr();
level l_1 = sort_level(binding_body(binding_body(mtype)));