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

fix(kernel/default_converter): avoid assertion violation when normalizing type incorrect expressions

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-22 16:17:43 -08:00
parent 753b9dcd75
commit a8554b6ed9
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/default_converter.cpp
View file

@ -123,7 +123,8 @@ bool default_converter::is_opaque(declaration const & d) const {
expr default_converter::unfold_name_core(expr e, unsigned w) {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e))) {
if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w)
if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w &&
length(const_levels(e)) == d->get_num_univ_params())
return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w);
}
}