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

fix(kernel/type_checker): bug in new is_opaque method

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-25 12:24:14 -07:00
parent 1d92097781
commit 28796593e3
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/kernel/type_checker.cpp
View file

@ -414,7 +414,7 @@ bool type_checker::is_opaque(declaration const & d) const {
bool type_checker::is_opaque(expr const & c) const { bool type_checker::is_opaque(expr const & c) const {
lean_assert(is_constant(c)); lean_assert(is_constant(c));
if (auto d = m_env.find(const_name(c))) if (auto d = m_env.find(const_name(c)))
return is_opaque(*d); return d->is_definition() && is_opaque(*d);
else else
return true; return true;
} }