max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/type_context): prevent assertion violation

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-03 18:43:55 -07:00
parent b79a8ddd25
commit e9d2d51760
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/type_context.cpp
View file

@ -411,10 +411,12 @@ expr type_context::whnf_core(expr const & e) {
/* Remark: we do not unfold Constants eagerly in this method */
return e;
case expr_kind::Local:
if (auto d = m_lctx.get_local_decl(e)) {
if (auto v = d->get_value()) {
/* zeta-reduction */
return whnf_core(*v);
if (is_local_decl_ref(e)) {
if (auto d = m_lctx.get_local_decl(e)) {
if (auto v = d->get_value()) {
/* zeta-reduction */
return whnf_core(*v);
}
}
}
return e;